PROOF: add checker for output parameters

sipma · sipma · commit 4d8a418db200 · 2025-11-12T23:32:12.000-08:00
diff --git a/chc/cmdline/juliet/JulietTestScoring.py b/chc/cmdline/juliet/JulietTestScoring.py
@@ -185,7 +185,7 @@ def f(spo: "CFunctionPO") -> None:
                 if sev is None:
                     sevtxt = "?"
                 else:
-                    sevtxt = spo.get_display_prefix() + "  " + sev
+                    sevtxt = spo.get_display_prefix() + "  " + str(sev)
                 lines.append(
                     "     C:"
                     + str(spo.line).rjust(3)
@@ -213,7 +213,7 @@ def testppo_results_tostring(
                 if ev is None:
                     evstr = "?"
                 else:
-                    evstr = ppo.get_display_prefix() + "  " + ev
+                    evstr = ppo.get_display_prefix() + "  " + str(ev)
                 lines.append(
                     "    "
                     + str(ppo.line).rjust(3)
diff --git a/chc/proof/CFunctionCallsiteSPO.py b/chc/proof/CFunctionCallsiteSPO.py
@@ -39,7 +39,7 @@
     from chc.proof.CFunPODictionaryRecord import CFunPOType
     from chc.proof.CFunctionProofs import CFunctionProofs
     from chc.proof.CProofDependencies import CProofDependencies
-    from chc.proof.CProofDiagnostic import CProofDiagnostic
+    from chc.proof.CProofDiagnostic import CProofDiagnostic, SituatedMsg
     from chc.proof.SPOType import CallsiteSPOType
 
 
@@ -52,7 +52,7 @@ def __init__(
             potype: "CFunPOType",
             status: str = "open",
             deps: Optional["CProofDependencies"] = None,
-            expl: Optional[str] = None,
+            expl: Optional["SituatedMsg"] = None,
             diag: Optional["CProofDiagnostic"] = None) -> None:
         CFunctionPO.__init__(self, cproofs, potype, status, deps, expl, diag)
 
diff --git a/chc/proof/CFunctionCallsiteSPOs.py b/chc/proof/CFunctionCallsiteSPOs.py
@@ -43,7 +43,7 @@
 from chc.proof.CFunctionCallsiteSPO import CFunctionCallsiteSPO
 from chc.proof.CFunctionPO import po_status
 from chc.proof.CProofDependencies import CProofDependencies
-from chc.proof.CProofDiagnostic import CProofDiagnostic
+from chc.proof.CProofDiagnostic import CProofDiagnostic, SituatedMsg
 
 import chc.util.fileutil as UF
 from chc.util.loggingutil import chklogger
@@ -233,8 +233,10 @@ def spos(self) -> Dict[int, List[CFunctionCallsiteSPO]]:
                             deps = CProofDependencies(self.cproofs, xpo)
                             status = po_status[xpo.get("s", "o")]
                             xexpl = xpo.find("e")
-                            expl = None if xexpl is None else xexpl.get("txt")
-                            diagnostic = CProofDiagnostic(xpo.find("d"))
+                            expl = (
+                                None if xexpl is None
+                                else SituatedMsg(self.cfun.cdictionary, xexpl))
+                            diagnostic = CProofDiagnostic(self.cproofs, xpo.find("d"))
                             self._spos[int(xapid)].append(
                                 CFunctionCallsiteSPO(
                                     self.cproofs,
diff --git a/chc/proof/CFunctionLocalSPO.py b/chc/proof/CFunctionLocalSPO.py
@@ -38,7 +38,7 @@
     from chc.proof.CFunctionProofs import CFunctionProofs
     from chc.proof.CFunPODictionaryRecord import CFunPOType
     from chc.proof.CProofDependencies import CProofDependencies
-    from chc.proof.CProofDiagnostic import CProofDiagnostic
+    from chc.proof.CProofDiagnostic import CProofDiagnostic, SituatedMsg
 
 
 class CFunctionLocalSPO(CFunctionPO):
@@ -49,7 +49,7 @@ def __init__(
             potype: "CFunPOType",
             status: str = "open",
             deps: Optional["CProofDependencies"] = None,
-            expl: Optional[str] = None,
+            expl: Optional["SituatedMsg"] = None,
             diag: Optional["CProofDiagnostic"] = None) -> None:
         CFunctionPO.__init__(self, cproofs, potype, status, deps, expl, diag)
 
diff --git a/chc/proof/CFunctionPO.py b/chc/proof/CFunctionPO.py
@@ -47,7 +47,7 @@
     from chc.proof.CFunPODictionary import CFunPODictionary
     from chc.proof.CPOPredicate import CPOPredicate
     from chc.proof.CProofDependencies import CProofDependencies
-    from chc.proof.CProofDiagnostic import CProofDiagnostic
+    from chc.proof.CProofDiagnostic import CProofDiagnostic, SituatedMsg
     from chc.proof.SPOType import SPOType
 
 
@@ -72,7 +72,7 @@ def __init__(
             potype: CFunPOType,
             status: str = "open",
             deps: Optional["CProofDependencies"] = None,
-            expl: Optional[str] = None,
+            expl: Optional["SituatedMsg"] = None,
             diag: Optional["CProofDiagnostic"] = None) -> None:
         self._cproofs = cproofs
         self._potype = potype
@@ -182,7 +182,7 @@ def has_dependencies(self) -> bool:
         return self._dependencies is not None
 
     @property
-    def explanation(self) -> Optional[str]:
+    def explanation(self) -> Optional["SituatedMsg"]:
         return self._explanation
 
     def has_explanation(self) -> bool:
@@ -364,7 +364,7 @@ def write_xml(self, cnode: ET.Element) -> None:
             self.dependencies.write_xml(cnode)
         if self.explanation is not None:
             enode = ET.Element("e")
-            enode.set("txt", self.explanation)
+            enode.set("txt", self.explanation.msg)
             cnode.append(enode)
         if self.has_diagnostic():
             dnode = ET.Element("d")
diff --git a/chc/proof/CFunctionPPO.py b/chc/proof/CFunctionPPO.py
@@ -38,7 +38,7 @@
     from chc.proof.CFunctionProofs import CFunctionProofs
     from chc.proof.CFunPODictionaryRecord import CFunPOType
     from chc.proof.CProofDependencies import CProofDependencies
-    from chc.proof.CProofDiagnostic import CProofDiagnostic
+    from chc.proof.CProofDiagnostic import CProofDiagnostic, SituatedMsg
 
 
 class CFunctionPPO(CFunctionPO):
@@ -50,7 +50,7 @@ def __init__(
             ppotype: "CFunPOType",
             status: str = "open",
             deps: Optional["CProofDependencies"] = None,
-            expl: Optional[str] = None,
+            expl: Optional["SituatedMsg"] = None,
             diag: Optional["CProofDiagnostic"] = None) -> None:
         CFunctionPO.__init__(self, cproofs, ppotype, status, deps, expl, diag)
 
diff --git a/chc/proof/CFunctionPPOs.py b/chc/proof/CFunctionPPOs.py
@@ -34,7 +34,7 @@
 
 from chc.proof.CFunctionPPO import CFunctionPPO
 from chc.proof.CProofDependencies import CProofDependencies
-from chc.proof.CProofDiagnostic import CProofDiagnostic
+from chc.proof.CProofDiagnostic import CProofDiagnostic, SituatedMsg
 
 import chc.util.fileutil as UF
 
@@ -90,12 +90,13 @@ def ppos(self) -> Dict[int, CFunctionPPO]:
                 id = ppotype.index
                 status = po_status[xp.get("s", "o")]
                 deps = CProofDependencies(self.cproofs, xp)
-                diagnostic = CProofDiagnostic(xp.find("d"))
+                diagnostic = CProofDiagnostic(self.cproofs, xp.find("d"))
 
                 # get explanation
                 enode = xp.find("e")
                 if enode is not None:
-                    expl: Optional[str] = enode.get("txt", "")
+                    expl: Optional[SituatedMsg] = SituatedMsg(
+                        self.cfun.cdictionary, enode)
                 else:
                     expl = None
 
diff --git a/chc/proof/CFunctionReturnsiteSPO.py b/chc/proof/CFunctionReturnsiteSPO.py
@@ -38,7 +38,7 @@
     from chc.proof.CFunctionReturnsiteSPOs import CFunctionReturnsiteSPOs
     from chc.proof.CFunPODictionaryRecord import CFunPOType
     from chc.proof.CProofDependencies import CProofDependencies
-    from chc.proof.CProofDiagnostic import CProofDiagnostic
+    from chc.proof.CProofDiagnostic import CProofDiagnostic, SituatedMsg
     from chc.proof.SPOType import SPOType
 
 
@@ -51,7 +51,7 @@ def __init__(
             potype: "CFunPOType",
             status: str = "open",
             deps: Optional["CProofDependencies"] = None,
-            expl: Optional[str] = None,
+            expl: Optional["SituatedMsg"] = None,
             diag: Optional["CProofDiagnostic"] = None) -> None:
         CFunctionPO.__init__(
             self, crspos.cproofs, potype, status, deps, expl, diag)
diff --git a/chc/proof/CFunctionReturnsiteSPOs.py b/chc/proof/CFunctionReturnsiteSPOs.py
@@ -39,7 +39,7 @@
 
 from chc.proof.CFunctionReturnsiteSPO import CFunctionReturnsiteSPO
 from chc.proof.CProofDependencies import CProofDependencies
-from chc.proof.CProofDiagnostic import CProofDiagnostic
+from chc.proof.CProofDiagnostic import CProofDiagnostic, SituatedMsg
 
 import chc.util.fileutil as UF
 
@@ -107,8 +107,10 @@ def spos(self) -> Dict[int, List[CFunctionReturnsiteSPO]]:
                         deps = CProofDependencies(self.cproofs, xpo)
                         status = po_status[xpo.get("s", "o")]
                         xexpl = xpo.find("e")
-                        expl = None if xexpl is None else xexpl.get("txt")
-                        diagnostic = CProofDiagnostic(xpo.find("d"))
+                        expl = (
+                            None if xexpl is None
+                            else SituatedMsg(self.cfun.cdictionary, xexpl))
+                        diagnostic = CProofDiagnostic(self.cproofs, xpo.find("d"))
                         self._spos[ipc].append(
                             CFunctionReturnsiteSPO(
                                 self, spotype, status, deps, expl, diagnostic))
diff --git a/chc/proof/CFunctionSPOs.py b/chc/proof/CFunctionSPOs.py
@@ -40,7 +40,7 @@
 from chc.proof.CFunctionPO import CFunctionPO
 from chc.proof.CFunctionPO import po_status
 from chc.proof.CProofDependencies import CProofDependencies
-from chc.proof.CProofDiagnostic import CProofDiagnostic
+from chc.proof.CProofDiagnostic import CProofDiagnostic, SituatedMsg
 
 from chc.util.loggingutil import chklogger
 
@@ -103,9 +103,11 @@ def local_spos(self) -> Dict[int, CFunctionLocalSPO]:
                 for xpo in xlspos.findall("po"):
                     spotype = self.podictionary.read_xml_spo_type(xpo)
                     xexpl = xpo.find("e")
-                    expl = None if xexpl is None else xexpl.get("txt")
+                    expl = (
+                        None if xexpl is None
+                        else SituatedMsg(self.cfun.cdictionary, xexpl))
                     deps = CProofDependencies(self.cproofs, xpo)
-                    diagnostic = CProofDiagnostic(xpo.find("d"))
+                    diagnostic = CProofDiagnostic(self.cproofs, xpo.find("d"))
                     status = po_status[xpo.get("s", "o")]
                     self._localspos[spotype.po_index] = CFunctionLocalSPO(
                         self.cproofs, spotype, status, deps, expl, diagnostic)
diff --git a/chc/proof/CProofDiagnostic.py b/chc/proof/CProofDiagnostic.py
@@ -32,15 +32,88 @@
 
 from typing import Dict, List, Optional, TYPE_CHECKING
 
+if TYPE_CHECKING:
+    from chc.app.CDictionary import CDictionary
+    from chc.app.CFunction import CFunction
+    from chc.proof.CFunctionProofs import CFunctionProofs
+
+
+class SituatedMsg:
+
+    def __init__(self, cd: "CDictionary", xnode: ET.Element) -> None:
+        self._cd = cd
+        self._xnode = xnode
+
+    @property
+    def cd(self) -> "CDictionary":
+        return self._cd
+
+    @property
+    def msg(self) -> str:
+        result = self._xnode.get("t")
+        if result is None:
+            return self._xnode.get("txt", "?")
+        else:
+            return result
+
+    @property
+    def file(self) -> Optional[str]:
+        xfile = self._xnode.get("file")
+        if xfile is not None:
+            return self.cd.get_string(int(xfile))
+        return None
+
+    @property
+    def line(self) -> Optional[int]:
+        xline = self._xnode.get("line")
+        if xline is not None:
+            return int(xline)
+        return None
+
+    @property
+    def detail(self) -> Optional[str]:
+        xdetail = self._xnode.get("detail")
+        if xdetail is not None:
+            return self.cd.get_string(int(xdetail))
+        return None
+
+    @property
+    def is_situated(self) -> bool:
+        return (
+            self.file is not None
+            and self.line is not None
+            and self.detail is not None)
+
+    def __str__(self) -> str:
+        if self.is_situated:
+            return self.msg + " (" + str(self.line) + ": " + str(self.detail) + ")"
+        else:
+            return self.msg
+
 
 class CProofDiagnostic:
 
-    def __init__(self, xnode: Optional[ET.Element]) -> None:
+    def __init__(
+            self, cproofs: "CFunctionProofs", xnode: Optional[ET.Element]
+    ) -> None:
+        self._cproofs = cproofs
         self._xnode = xnode
         self._invsmap: Optional[Dict[int, List[int]]] = None
-        self._amsgs: Optional[Dict[int, List[str]]] = None
+        self._amsgs: Optional[Dict[int, List[SituatedMsg]]] = None
         self._kmsgs: Optional[Dict[str, List[str]]] = None
-        self._msgs: Optional[List[str]] = None
+        self._msgs: Optional[List[SituatedMsg]] = None
+
+    @property
+    def cproofs(self) -> "CFunctionProofs":
+        return self._cproofs
+
+    @property
+    def cfun(self) -> "CFunction":
+        return self.cproofs.cfun
+
+    @property
+    def cd(self) -> "CDictionary":
+        return self.cfun.cdictionary
 
     @property
     def invsmap(self) -> Dict[int, List[int]]:
@@ -63,19 +136,20 @@ def invsmap(self) -> Dict[int, List[int]]:
         return self._invsmap
 
     @property
-    def msgs(self) -> List[str]:
+    def msgs(self) -> List[SituatedMsg]:
         """Returns general diagnostics pertaining to the proof obligation."""
 
         if self._msgs is None:
             self._msgs = []
             if self._xnode is not None:
                 mnode = self._xnode.find("msgs")
                 if mnode is not None:
-                    self._msgs = [x.get("t", "") for x in mnode.findall("msg")]
+                    self._msgs = [
+                        SituatedMsg(self.cd, x) for x in mnode.findall("msg")]
         return self._msgs
 
     @property
-    def argument_msgs(self) -> Dict[int, List[str]]:
+    def argument_msgs(self) -> Dict[int, List[SituatedMsg]]:
         """Returns argument-specific diagnostic messages.
 
         Note: argument index starts at 1.
@@ -89,7 +163,8 @@ def argument_msgs(self) -> Dict[int, List[str]]:
                     for n in anode.findall("arg"):
                         xargindex = n.get("a")
                         if xargindex is not None:
-                            msgs = [x.get("t", "") for x in n.findall("msg")]
+                            msgs = [
+                                SituatedMsg(self.cd, x) for x in n.findall("msg")]
                             self._amsgs[int(xargindex)] = msgs
         return self._amsgs
 
@@ -132,9 +207,9 @@ def write_xml(self, dnode: ET.Element) -> None:
         for arg in self.argument_msgs:
             anode = ET.Element("arg")
             anode.set("a", str(arg))
-            for t in self.argument_msgs[arg]:
+            for msg in self.argument_msgs[arg]:
                 tnode = ET.Element("msg")
-                tnode.set("t", t)
+                tnode.set("t", msg.msg)
                 anode.append(tnode)
             aanode.append(anode)
         for key in self.keyword_msgs:
@@ -145,13 +220,13 @@ def write_xml(self, dnode: ET.Element) -> None:
                 tnode.set("t", t)
                 knode.append(tnode)
             kknode.append(knode)
-        for t in self.msgs:
+        for msg in self.msgs:
             mnode = ET.Element("msg")
-            mnode.set("t", t)
+            mnode.set("t", msg.msg)
             mmnode.append(mnode)
         dnode.extend([inode, mmnode, aanode, kknode])
 
     def __str__(self) -> str:
         if len(self.msgs) == 0:
             return "no diagnostic messages"
-        return "\n".join(self.msgs)
+        return "\n".join(str(m) for m in self.msgs)
diff --git a/chc/proof/OutputParameterChecker.py b/chc/proof/OutputParameterChecker.py
diff --git a/chc/reporting/ProofObligations.py b/chc/reporting/ProofObligations.py
