Skip to content

Performance #64

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
sipma merged 23 commits into from
Feb 3, 2026
Merged

Performance #64

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
23 commits
Select commit Hold shift + click to select a range
cba47b2
CMD: add command-line option to control status of system includes
sipma Oct 25, 2025
6f97471
PROOF: add support for output-parameter predicates
sipma Nov 9, 2025
32fa1c8
APP: add analysis info to function
sipma Nov 9, 2025
c6f5e62
CMD: add cmdline options to choose analysis
sipma Nov 9, 2025
4d8a418
PROOF: add checker for output parameters
sipma Nov 13, 2025
aee66d3
PROOF: add unique-pointer predicate
sipma Nov 15, 2025
366a572
extend cil-source pretty printer
sipma Nov 18, 2025
5ccf5a8
PROOF: add return values to output parameter results
sipma Nov 20, 2025
0b1fb21
CMD: delegate to analysis digests
sipma Dec 6, 2025
b8040a0
CHC:INSTR: ignore vardecl for now
sipma Dec 6, 2025
d07415d
DECL: replace exception on unrecognized InitInfo by printed msg
sipma Dec 6, 2025
bf450d3
replace analysis-info with analysis-digest
sipma Dec 6, 2025
5d24d1f
UF: add file utility for analysis-digest file
sipma Dec 6, 2025
16ec171
PROOF: output-parameter analysis digest support
sipma Dec 6, 2025
bad32a4
APP: allow for possibility of missing ppo's and invariants
sipma Dec 8, 2025
5d9f0f2
CMD: add investigate command for projects
sipma Dec 8, 2025
728c20d
PROOF: change representation for rejection reason
sipma Dec 18, 2025
c7c7f36
CMD: add cmd to show cil-based source code for project file
sipma Dec 18, 2025
47a2aad
APP: add offset-info
sipma Feb 2, 2026
1c41aa9
APP: add offset-info
sipma Feb 2, 2026
31ebfdf
CMD:top-level integration of output-parameter results
sipma Feb 2, 2026
53331ef
PROOF:supply results for integration of output-parameter analysis
sipma Feb 2, 2026
98d0df3
Merge branch 'master' into performance
sipma Feb 2, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
44 changes: 44 additions & 0 deletions chc/app/CApplication.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -54,6 +54,7 @@
if TYPE_CHECKING:
from chc.app.CFunction import CFunction
from chc.app.CInstr import CCallInstr
from chc.proof.CandidateOutputParameter import CandidateOutputParameter
from chc.proof.CFunctionCallsiteSPOs import CFunctionCallsiteSPOs
from chc.proof.CFunctionPO import CFunctionPO

Expand Down Expand Up @@ -93,12 +94,14 @@ def __init__(
targetpath: str,
contractpath: str,
singlefile: bool = False,
keep_system_includes: bool = False,
excludefiles: List[str] = []) -> None:
self._projectpath = projectpath
self._projectname = projectname
self._targetpath = targetpath
self._contractpath = contractpath
self._singlefile = singlefile
self._keep_system_includes = keep_system_includes
self._excludefiles = excludefiles
self._indexmanager = IndexManager(singlefile)
self._globalcontract: Optional[CGlobalContract] = None
Expand Down Expand Up @@ -138,6 +141,19 @@ def globalcontract(self) -> CGlobalContract:
def is_singlefile(self) -> bool:
return self._singlefile

@property
def keep_system_includes(self) -> bool:
"""Returns true if functions from the system path ('/') must be included

This property is false by default and must be enabled via a command-line
option.

It is intended to, by default, filter out functions defined in header
files, that would otherwise be included in every source file.
"""

return self._keep_system_includes

@property
def excludefiles(self) -> List[str]:
return self._excludefiles
Expand Down Expand Up @@ -300,6 +316,34 @@ def g(fi: CFile) -> None:

self.iter_files_parallel(g, maxprocesses)

def check_digests(self) -> bool:
for cfile in list(self.cfiles):
for cfun in cfile.get_functions():
if cfun.analysis_digests.is_active:
return True
return False

def outputparameters(self) -> Dict[str, List["CandidateOutputParameter"]]:
result: Dict[str, List["CandidateOutputParameter"]] = {}
for cfile in list(self.cfiles):
for cfun in cfile.get_functions():
result[cfun.name] = cfun.analysis_digests.outputparameters()
return result

def viable_outputparameters(self) -> Dict[str, List["CandidateOutputParameter"]]:
result: Dict[str, List["CandidateOutputParameter"]] = {}
for cfile in list(self.cfiles):
for cfun in cfile.get_functions():
result[cfun.name] = cfun.analysis_digests.viable_outputparameters()
return result

def maybe_outputparameters(self) -> Dict[str, List["CandidateOutputParameter"]]:
result: Dict[str, List["CandidateOutputParameter"]] = {}
for cfile in list(self.cfiles):
for cfun in cfile.get_functions():
result[cfun.name] = cfun.analysis_digests.maybe_outputparameters()
return result

def resolve_vid_function(
self, filevar: FileVarReference) -> Optional["CFunction"]:
"""Returns the function def for the local file-index fid and vid.
Expand Down
54 changes: 54 additions & 0 deletions chc/app/CAttributes.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -113,6 +113,9 @@ def is_index(self) -> bool:
def is_question(self) -> bool:
return False

def accept(self, visitor: "CVisitor") -> None:
raise UF.CHCError("visitor not yet implemented for " + str(self))

def __str__(self) -> str:
return "attrparam:" + self.tags[0]

Expand All @@ -135,6 +138,9 @@ def intvalue(self) -> int:
def is_int(self) -> bool:
return True

def accept(self, visitor: "CVisitor") -> None:
visitor.visit_attr_int(self)

def __str__(self) -> str:
return "aint(" + str(self.intvalue) + ")"

Expand All @@ -157,6 +163,9 @@ def stringvalue(self) -> str:
def is_str(self) -> bool:
return True

def accept(self, visitor: "CVisitor") -> None:
visitor.visit_attr_str(self)

def __str__(self) -> str:
return "astr(" + str(self.stringvalue) + ")"

Expand Down Expand Up @@ -184,6 +193,9 @@ def params(self) -> List[CAttr]:
def is_cons(self) -> bool:
return True

def accept(self, visitor: "CVisitor") -> None:
visitor.visit_attr_cons(self)

def __str__(self) -> str:
return "acons(" + str(self.name) + ")"

Expand All @@ -206,6 +218,9 @@ def typ(self) -> "CTyp":
def is_sizeof(self) -> bool:
return True

def accept(self, visitor: "CVisitor") -> None:
visitor.visit_attr_sizeof(self)

def __str__(self) -> str:
return "asizeof(" + str(self.typ) + ")"

Expand All @@ -228,6 +243,9 @@ def param(self) -> CAttr:
def is_sizeofe(self) -> bool:
return True

def accept(self, visitor: "CVisitor") -> None:
visitor.visit_attr_sizeofe(self)

def __str__(self) -> str:
return "asizeofe(" + str(self.param) + ")"

Expand All @@ -250,6 +268,9 @@ def typsig(self) -> "CTypsig":
def is_sizeofs(self) -> bool:
return True

def accept(self, visitor: "CVisitor") -> None:
visitor.visit_attr_sizeofs(self)

def __str__(self) -> str:
return "asizeofs(" + str(self.typsig) + ")"

Expand All @@ -272,6 +293,9 @@ def typ(self) -> "CTyp":
def is_alignof(self) -> bool:
return True

def accept(self, visitor: "CVisitor") -> None:
visitor.visit_attr_alignof(self)

def __str__(self) -> str:
return "aalignof(" + str(self.typ) + ")"

Expand All @@ -294,6 +318,9 @@ def param(self) -> CAttr:
def is_alignofe(self) -> bool:
return True

def accept(self, visitor: "CVisitor") -> None:
visitor.visit_attr_alignofe(self)

def __str__(self) -> str:
return "aalignofe(" + str(self.param) + ")"

Expand All @@ -316,6 +343,9 @@ def typsig(self) -> "CTypsig":
def is_alignofs(self) -> bool:
return True

def accept(self, visitor: "CVisitor") -> None:
visitor.visit_attr_alignofs(self)

def __str__(self) -> str:
return "aalignofs(" + str(self.typsig) + ")"

Expand Down Expand Up @@ -343,6 +373,9 @@ def param(self) -> CAttr:
def is_unop(self) -> bool:
return True

def acecpt(self, visitor: "CVisitor") -> None:
visitor.visit_attr_unop(self)

def __str__(self) -> str:
return "aunop(" + self.op + "," + str(self.param) + ")"

Expand Down Expand Up @@ -375,6 +408,9 @@ def param2(self) -> CAttr:
def is_binop(self) -> bool:
return True

def accept(self, visitor: "CVisitor") -> None:
visitor.visit_attr_binop(self)

def __str__(self) -> str:
return (
"abinop("
Expand Down Expand Up @@ -410,6 +446,9 @@ def param(self) -> CAttr:
def is_dot(self) -> bool:
return True

def accept(self, visitor: "CVisitor") -> None:
visitor.visit_attr_dot(self)

def __str__(self) -> str:
return "adot(" + str(self.param) + "." + self.suffix + ")"

Expand All @@ -436,6 +475,9 @@ def param(self) -> CAttr:
def is_star(self) -> bool:
return True

def accept(self, visitor: "CVisitor") -> None:
visitor.visit_attr_star(self)

def __str__(self) -> str:
if self.index == self.args[0]:
return "astar()"
Expand All @@ -461,6 +503,9 @@ def param(self) -> CAttr:
def is_addrof(self) -> bool:
return True

def accept(self, visitor: "CVisitor") -> None:
visitor.visit_attr_addrof(self)

def __str__(self) -> str:
return "aaddrof(" + str(self.param) + ")"

Expand Down Expand Up @@ -488,6 +533,9 @@ def param2(self) -> CAttr:
def is_index(self) -> bool:
return True

def accept(self, visitor: "CVisitor") -> None:
visitor.visit_attr_index(self)

def __str__(self) -> str:
return "aindex(" + str(self.param1) + "," + str(self.param2) + ")"

Expand Down Expand Up @@ -516,6 +564,9 @@ def param2(self) -> CAttr:
def param3(self) -> CAttr:
return self.cd.get_attrparam(int(self.args[2]))

def accept(self, visitor: "CVisitor") -> None:
visitor.visit_attr_question(self)

def __str__(self) -> str:
return (
"aquestion("
Expand All @@ -541,6 +592,9 @@ def name(self) -> str:
def params(self) -> List[CAttr]:
return [self.cd.get_attrparam(int(i)) for i in self.args]

def accept(self, visitor: "CVisitor") -> None:
visitor.visit_attribute(self)

def __str__(self) -> str:
return self.name + ": " + ",".join([str(p) for p in self.params])

Expand Down
6 changes: 5 additions & 1 deletion chc/app/CCompInfo.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@
#
# Copyright (c) 2017-2020 Kestrel Technology LLC
# Copyright (c) 2020-2022 Henny B. Sipma
# 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
Expand Down Expand Up @@ -39,6 +39,7 @@
from chc.app.CDeclarations import CDeclarations
from chc.app.CFieldInfo import CFieldInfo
from chc.app.CGlobalDeclarations import CGlobalDeclarations
from chc.app.CVisitor import CVisitor


class CCompInfo(CDeclarationsRecord):
Expand Down Expand Up @@ -100,6 +101,9 @@ def name(self) -> str:
def field_strings(self) -> str:
return ":".join([f.fname for f in self.fields])

def accept(self, visitor: "CVisitor") -> None:
visitor.visit_compinfo(self)

def __str__(self) -> str:
lines = []
lines.append("struct " + self.name)
Expand Down
10 changes: 10 additions & 0 deletions chc/app/CContextDictionary.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down
7 changes: 7 additions & 0 deletions chc/app/CDictionary.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down
Loading