PROOF: add return values to output parameter results

Author: sipma

chc/app/CContextDictionary.py

@@ -88,6 +88,16 @@ def get_program_context(self, ix: int) -> ProgramContext:
     def get_program_context_map(self) -> Dict[int, IndexedTableValue]:
         return self.context_table.objectmap(self.get_program_context)
 
+    # ----------------- read_xml service ---------------------------------------
+
+    def read_xml_program_context(
+            self, node: ET.Element, tag: str = "ictxt") -> ProgramContext:
+        xtag = node.get(tag)
+        if xtag is not None:
+            return self.get_program_context(int(xtag))
+        else:
+            raise UF.CHCError(f"Xml element {node.tag} is missing attribute {tag}")
+
     # ----------------------- Printing -----------------------------------------
 
     def objectmap_to_string(self, name: str) -> str:

chc/app/CDictionary.py

@@ -268,6 +268,13 @@ def read_xml_exp(self, node: ET.Element, tag: str = "iexp") -> CExp:
         else:
             raise Exception('xml node was missing the tag "' + tag + '"')
 
+    def read_xml_exp_o(
+            self, node: ET.Element, tag: str = "iexp") -> Optional[CExp]:
+        xtag_o = node.get(tag)
+        if xtag_o is not None:
+            return self.get_exp(int(xtag_o))
+        return None
+
     def write_xml_exp_opt(
         self,
         node: ET.Element,

chc/app/CFileDeclarations.py

@@ -37,6 +37,7 @@
     List,
     Mapping,
     NoReturn,
+    Optional,
     Tuple,
     TYPE_CHECKING)
 import xml.etree.ElementTree as ET
@@ -92,6 +93,10 @@ def xget_int_attr(p: ET.Element, tag: str) -> int:
     return UF.xget_int_attr(p, tag, "CFileDeclarations")
 
 
+def xget_int_attr_o(node: ET.Element, tag: str) -> Optional[int]:
+    return UF.xget_int_attr_o(node, tag)
+
+
 class CFilename(CDeclarationsRecord):
 
     def __init__(self, decls: CDeclarations, ixval: IndexedTableValue):
@@ -266,6 +271,17 @@ def read_xml_location(
             return CLocation(self, itv)
         return self.get_location(index)
 
+    def read_xml_location_o(
+            self, xnode: ET.Element, tag: str = "iloc") -> Optional[CLocation]:
+        index = xget_int_attr_o(xnode, tag)
+        if index is not None:
+            if index == -1:
+                args = [-1, -1, -1]
+                itv = IndexedTableValue(-1, [], args)
+                return CLocation(self, itv)
+            return self.get_location(index)
+        return None
+
     # -------------------- Index items by category ---------------------------
 
     def index_filename(self, name: str) -> int:

chc/app/CFunction.py

@@ -35,9 +35,10 @@
 
 from chc.api.CFunctionApi import CFunctionApi
 
-from chc.app.CLocation import CLocation
 from chc.app.CFunDeclarations import CFunDeclarations
 from chc.app.CInstr import CCallInstr
+from chc.app.CFunctionReturnSite import CFunctionReturnSite
+from chc.app.CLocation import CLocation
 from chc.app.CStmt import CFunctionBody
 from chc.app.IndexManager import FileVarReference
 
@@ -159,6 +160,7 @@ def __init__(self, cfile: "CFile", xnode: ET.Element, fname: str) -> None:
         self._formals: Dict[int, "CVarInfo"] = {}  # vid -> CVarInfo
         self._locals: Dict[int, "CVarInfo"] = {}  # vid -> CVarInfo
         self._sbody: Optional[CFunctionBody] = None
+        self._returnsites: Optional[List[CFunctionReturnSite]] = None
         self._podictionary: Optional[CFunPODictionary] = None
         self._api: Optional[CFunctionApi] = None
         self._proofs: Optional[CFunctionProofs] = None
@@ -373,6 +375,36 @@ def podictionary(self) -> CFunPODictionary:
             self._podictionary = CFunPODictionary(self, pxnode)
         return self._podictionary
 
+    @property
+    def returnsites(self) -> List[CFunctionReturnSite]:
+        if self._returnsites is None:
+            self._returnsites = []
+            xsponode = UF.get_spo_xnode(
+                self.targetpath,
+                self.projectname,
+                self.cfilepath,
+                self.cfilename,
+                self.name)
+            if xsponode is None:
+                raise UF.CHCError(self.xmsg("spo file is missing"))
+            xxsponode = xsponode.find("spos")
+            if xxsponode is None:
+                raise UF.CHCError(self.xmsg("spo file has no spos element"))
+            xreturnsites = xxsponode.find("returnsites")
+            if xreturnsites is None:
+                raise UF.CHCError(
+                    self.xmsg("spo file has no returnsites element"))
+            for xreturnsite in xreturnsites.findall("rs"):
+                self._returnsites.append(CFunctionReturnSite(self, xreturnsite))
+        return self._returnsites
+
+    def get_returnsite(
+            self, ctxtid: int) -> Optional[CFunctionReturnSite]:
+        for rs in self.returnsites:
+            if rs.context.index == ctxtid:
+                return rs
+        return None
+
     @property
     def proofs(self) -> CFunctionProofs:
         if self._proofs is None:
@@ -397,22 +429,30 @@ def proofs(self) -> CFunctionProofs:
                 raise UF.CHCError(self.xmsg("spo file is missing"))
             xxsponode = xsponode.find("spos")
             if xxsponode is None:
-                raise UF.CHCError(self.xmsg("_spo file has no spos element"))
+                raise UF.CHCError(self.xmsg("spo file has no spos element"))
             self._proofs = CFunctionProofs(self, xxpponode, xxsponode)
         return self._proofs
 
     @property
     def analysis_info(self) -> CAnalysisInfo:
         if self._analysisinfo is None:
-            xpponode = UF.get_ppo_xnode(
-                self.targetpath,
-                self.projectname,
-                self.cfilepath,
-                self.cfilename,
-                self.name)
-            if xpponode is not None:
-                self._analysisinfo = (
-                    CAnalysisInfo(xpponode.find("analysis-info"), self))
+            if UF.has_ppo_file(
+                    self.targetpath,
+                    self.projectname,
+                    self.cfilepath,
+                    self.cfilename,
+                    self.name):
+                xpponode = UF.get_ppo_xnode(
+                    self.targetpath,
+                    self.projectname,
+                    self.cfilepath,
+                    self.cfilename,
+                    self.name)
+                if xpponode is not None:
+                    self._analysisinfo = (
+                        CAnalysisInfo(xpponode.find("analysis-info"), self))
+                else:
+                    self._analysisinfo = CAnalysisInfo(None, self)
             else:
                 self._analysisinfo = CAnalysisInfo(None, self)
         return self._analysisinfo

chc/app/CFunctionReturnSite.py

@@ -0,0 +1,92 @@
+# ------------------------------------------------------------------------------
+# CodeHawk C Analyzer
+# Author: Henny Sipma
+# ------------------------------------------------------------------------------
+# The MIT License (MIT)
+#
+# Copyright (c) 2025  Aarno Labs LLC
+#
+# Permission is hereby granted, free of charge, to any person obtaining a copy
+# of this software and associated documentation files (the "Software"), to deal
+# in the Software without restriction, including without limitation the rights
+# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+# copies of the Software, and to permit persons to whom the Software is
+# furnished to do so, subject to the following conditions:
+#
+# The above copyright notice and this permission notice shall be included in all
+# copies or substantial portions of the Software.
+#
+# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+# FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+# SOFTWARE.
+# ------------------------------------------------------------------------------
+
+import xml.etree.ElementTree as ET
+
+from typing import Optional, TYPE_CHECKING
+
+if TYPE_CHECKING:
+    from chc.app.CContext import ProgramContext
+    from chc.app.CContext import CContextDictionary
+    from chc.app.CDictionary import CDictionary
+    from chc.app.CExp import CExp
+    from chc.app.CFile import CFile
+    from chc.app.CFileDeclarations import CFileDeclarations
+    from chc.app.CFunction import CFunction
+    from chc.app.CLocation import CLocation
+
+
+class CFunctionReturnSite:
+
+    def __init__(self, cfun: "CFunction", xnode: ET.Element) -> None:
+        self._cfun = cfun
+        self._xnode = xnode
+
+    @property
+    def cfun(self) -> "CFunction":
+        return self._cfun
+
+    @property
+    def cdictionary(self) -> "CDictionary":
+        return self.cfun.cdictionary
+
+    @property
+    def cfile(self) -> "CFile":
+        return self.cfun.cfile
+
+    @property
+    def cfiledeclarations(self) -> "CFileDeclarations":
+        return self.cfile.declarations
+
+    @property
+    def contextdictionary(self) -> "CContextDictionary":
+        return self.cfile.contextdictionary
+
+    @property
+    def xnode(self) -> ET.Element:
+        return self._xnode
+
+    @property
+    def location(self) -> "CLocation":
+        return self.cfiledeclarations.read_xml_location(self.xnode)
+
+    @property
+    def returnexp(self) -> Optional["CExp"]:
+        return self.cdictionary.read_xml_exp_o(self.xnode)
+
+    @property
+    def context(self) -> "ProgramContext":
+        return self.contextdictionary.read_xml_program_context(self.xnode)
+
+    def __str__(self):
+        rexp = str(self.returnexp) if self.returnexp else ""
+        return (
+            "return " + rexp + " ("
+            + str(self.location.line) + ", " + str(self.location.byte)
+            + ") ("
+            + str(self.context)
+        )

chc/cmdline/c_file/cfileutil.py

@@ -653,14 +653,17 @@ def pofilter(po: "CFunctionPO") -> bool:
         print(RP.file_proofobligation_stats_tostring(cfile))
 
         if canalysis == "outputparameters":
+            print("\n\nOutput parameter analysis results:\n")
             for cfun in cfile.functions.values():
-                try:
-                    op_checker = OutputParameterChecker(cfun)
-                    print(str(op_checker))
-                except UF.CHCError as e:
-                    print("Skipping function " + cfun.name)
-                    continue
-
+                op_checker = OutputParameterChecker(cfun)
+                results = op_checker.results()
+                if len(results) > 0:
+                    print("\nFunction: " + cfun.name + ": ")
+                    for result in results:
+                        if result.is_success():
+                            print(result.success_str())
+                        else:
+                            print(result.failure_str())
         exit(0)
 
     for fnname in cfunctions: