PROOF: add support for output-parameter predicates

Author: sipma

chc/proof/CFilePredicateDictionary.py

@@ -194,6 +194,10 @@ def f(index: int, tags: List[str], args: List[int]) -> PO.CPOPredicate:
             p = cast(PO.CPOInitialized, p)
             args = [self.dictionary.index_lval(p.lval, subst=subst)]
 
+        elif p.is_locally_initialized:
+            p = cast(PO.CPOLocallyInitialized, p)
+            args = [self.dictionary.index_lval(p.lval, subst=subst)]
+
         elif p.is_initialized_range:
             p = cast(PO.CPOInitializedRange, p)
             args = [

chc/proof/CFilePredicateRecord.py

@@ -4,7 +4,7 @@
 # ------------------------------------------------------------------------------
 # The MIT License (MIT)
 #
-# Copyright (c) 2023-2024  Aarno Labs LLC
+# Copyright (c) 2023-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
@@ -37,6 +37,7 @@
 if TYPE_CHECKING:
     from chc.app.CDictionary import CDictionary
     from chc.app.CFile import CFile
+    from chc.app.CFileDeclarations import CFileDeclarations
     from chc.proof.CFilePredicateDictionary import CFilePredicateDictionary
 
 
@@ -59,6 +60,10 @@ def pd(self) -> "CFilePredicateDictionary":
     def cd(self) -> "CDictionary":
         return self.pd.dictionary
 
+    @property
+    def cdeclarations(self) -> "CFileDeclarations":
+        return self.cfile.declarations
+
     @property
     def cfile(self) -> "CFile":
         return self.pd.cfile

chc/proof/CFunctionProofs.py

@@ -30,7 +30,7 @@
 
 import xml.etree.ElementTree as ET
 
-from typing import Callable, List, Optional, TYPE_CHECKING
+from typing import Callable, cast, List, Optional, TYPE_CHECKING
 
 from chc.proof.CFunctionCallsiteSPOs import CFunctionCallsiteSPOs
 from chc.proof.CFunctionPO import CFunctionPO
@@ -44,6 +44,10 @@
     from chc.app.CApplication import CApplication
     from chc.app.CFile import CFile
     from chc.app.CFunction import CFunction
+    from chc.proof.CPOPredicate import (
+        CPOLocallyInitialized,
+        CPOOutputParameterInitialized,
+        CPOOutputParameterUnaltered)
 
 
 class CFunctionProofs:
@@ -240,6 +244,23 @@ def _get_spos(self, force=False):
                     + self.cfile.name
                 )
 
+    def get_output_parameter_ppos(self, vname: str) -> List[CFunctionPO]:
+        result: List[CFunctionPO] = []
+        for ppo in self.ppolist:
+            if ppo.predicate.is_locally_initialized:
+                vinfo = cast("CPOLocallyInitialized", ppo.predicate).varinfo
+                if vinfo.vname == vname:
+                    result.append(ppo)
+            elif ppo.predicate.is_output_parameter_initialized:
+                vinfo = cast("CPOOutputParameterInitialized", ppo.predicate).varinfo
+                if vinfo.vname == vname:
+                    result.append(ppo)
+            elif ppo.predicate.is_output_parameter_unaltered:
+                vinfo = cast("CPOOutputParameterUnaltered", ppo.predicate).varinfo
+                if vinfo.vname == vname:
+                    result.append(ppo)
+        return result
+
     def _save_spos(self, cnode: ET.Element) -> None:
         UF.save_spo_file(
             self.targetpath,

chc/proof/CPOPredicate.py

@@ -40,7 +40,9 @@
     from chc.app.CExp import CExp, CExpLval
     from chc.app.CLHost import CLHostVar
     from chc.app.CLval import CLval
+    from chc.app.COffset import COffset
     from chc.app.CTyp import CTyp
+    from chc.app.CVarInfo import CVarInfo
     from chc.proof.CFilePredicateDictionary import CFilePredicateDictionary
 
 
@@ -71,12 +73,15 @@
     'iu': 'int-underflow',
     'iub': 'index-upper-bound',
     'lb': 'lower-bound',
+    'li': 'locally-initialized',
     'nm': 'new-memory',
     'nn': 'not-null',
     'nneg': 'non-negative',
     'no': 'no-overlap',
     'nt': 'null-terminated',
     'null': 'null',
+    'opi': 'output_parameter-initialized',
+    'opu': 'output_parameter-unaltered',
     'pc': 'pointer-cast',
     'plb': 'ptr-lower-bound',
     'pre': 'precondition',
@@ -180,6 +185,10 @@ def is_index_upper_bound(self) -> bool:
     def is_initialized(self) -> bool:
         return False
 
+    @property
+    def is_locally_initialized(self) -> bool:
+        return False
+
     @property
     def is_initialized_range(self) -> bool:
         return False
@@ -224,6 +233,14 @@ def is_null(self) -> bool:
     def is_null_terminated(self) -> bool:
         return False
 
+    @property
+    def is_output_parameter_initialized(self) -> bool:
+        return False
+
+    @property
+    def is_output_parameter_unaltered(self) -> bool:
+        return False
+
     @property
     def is_pointer_cast(self) -> bool:
         return False
@@ -962,6 +979,48 @@ def __str__(self) -> str:
         return "initialized(" + str(self.lval) + ")"
 
 
+@pdregistry.register_tag("li", CPOPredicate)
+class CPOLocallyInitialized(CPOPredicate):
+    """locally initialized(lval): location initialized within the function.
+
+    - args[0]: index of lval in cdictionary
+    """
+
+    def __init__(
+            self, pd: "CFilePredicateDictionary", ixval: IT.IndexedTableValue
+            ) -> None:
+        CPOPredicate.__init__(self, pd, ixval)
+
+    @property
+    def varinfo(self) -> "CVarInfo":
+        return self.cdeclarations.get_varinfo(self.args[0])
+
+    @property
+    def lval(self) -> "CLval":
+        return self.cd.get_lval(self.args[1])
+
+    @property
+    def is_locally_initialized(self) -> bool:
+        return True
+
+    def has_variable(self, vid: int) -> bool:
+        return self.lval.has_variable(vid)
+
+    def has_variable_deref(self, vid: int) -> bool:
+        return self.lval.has_variable_deref(vid)
+
+    def has_ref_type(self) -> bool:
+        return self.lval.has_ref_type()
+
+    def __str__(self) -> str:
+        return (
+            "locally-initialized("
+            + str(self.varinfo.vname)
+            + ", "
+            + str(self.lval)
+            + ")")
+
+
 @pdregistry.register_tag("ir", CPOPredicate)
 class CPOInitializedRange(CPOPredicate):
     """initialized-range(exp, size): the memory range starting at the address
@@ -2162,3 +2221,73 @@ def has_variable(self, vid: int) -> bool:
 
     def __str__(self) -> str:
         return "preserves-value(" + str(self.exp) + ")"
+
+
+@pdregistry.register_tag("opi", CPOPredicate)
+class CPOOutputParameterInitialized(CPOPredicate):
+    """
+
+    - args[0]: index of varinfo in cdecls
+    """
+    def __init__(
+            self, pd: "CFilePredicateDictionary", ixval: IT.IndexedTableValue
+    ) -> None:
+        CPOPredicate.__init__(self, pd, ixval)
+
+    @property
+    def varinfo(self) -> "CVarInfo":
+        return self.cdeclarations.get_varinfo(self.args[0])
+
+    @property
+    def offset(self) -> "COffset":
+        return self.cd.get_offset(self.args[1])
+
+    @property
+    def is_output_parameter_initialized(self) -> bool:
+        return True
+
+    def has_variable(self, vid: int) -> bool:
+        return self.varinfo.vid == vid
+
+    def __str__(self) -> str:
+        return (
+            "output_parameter-initialized("
+            + str(self.varinfo.vname)
+            + ", "
+            + str(self.offset)
+            + ")")
+
+
+@pdregistry.register_tag("opu", CPOPredicate)
+class CPOOutputParameterUnaltered(CPOPredicate):
+    """
+
+    - args[0]: index of varinfo in cdecls
+    """
+    def __init__(
+            self, pd: "CFilePredicateDictionary", ixval: IT.IndexedTableValue
+    ) -> None:
+        CPOPredicate.__init__(self, pd, ixval)
+
+    @property
+    def varinfo(self) -> "CVarInfo":
+        return self.cdeclarations.get_varinfo(self.args[0])
+
+    @property
+    def offset(self) -> "COffset":
+        return self.cd.get_offset(self.args[1])
+
+    @property
+    def is_output_parameter_unaltered(self) -> bool:
+        return True
+
+    def has_variable(self, vid: int) -> bool:
+        return self.varinfo.vid == vid
+
+    def __str__(self) -> str:
+        return (
+            "output_parameter-unaltered("
+            + str(self.varinfo.vname)
+            + ", "
+            + str(self.offset)
+            + ")")