Skip to content

Commit db010d1

Browse files
authored
Merge pull request #64 from static-analysis-engineering/performance
Support for output-parameter analysis.
2 parents 202ac80 + 98d0df3 commit db010d1

54 files changed

Lines changed: 3330 additions & 210 deletions

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

chc/app/CApplication.py

Lines changed: 44 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -54,6 +54,7 @@
5454
if TYPE_CHECKING:
5555
from chc.app.CFunction import CFunction
5656
from chc.app.CInstr import CCallInstr
57+
from chc.proof.CandidateOutputParameter import CandidateOutputParameter
5758
from chc.proof.CFunctionCallsiteSPOs import CFunctionCallsiteSPOs
5859
from chc.proof.CFunctionPO import CFunctionPO
5960

@@ -93,12 +94,14 @@ def __init__(
9394
targetpath: str,
9495
contractpath: str,
9596
singlefile: bool = False,
97+
keep_system_includes: bool = False,
9698
excludefiles: List[str] = []) -> None:
9799
self._projectpath = projectpath
98100
self._projectname = projectname
99101
self._targetpath = targetpath
100102
self._contractpath = contractpath
101103
self._singlefile = singlefile
104+
self._keep_system_includes = keep_system_includes
102105
self._excludefiles = excludefiles
103106
self._indexmanager = IndexManager(singlefile)
104107
self._globalcontract: Optional[CGlobalContract] = None
@@ -138,6 +141,19 @@ def globalcontract(self) -> CGlobalContract:
138141
def is_singlefile(self) -> bool:
139142
return self._singlefile
140143

144+
@property
145+
def keep_system_includes(self) -> bool:
146+
"""Returns true if functions from the system path ('/') must be included
147+
148+
This property is false by default and must be enabled via a command-line
149+
option.
150+
151+
It is intended to, by default, filter out functions defined in header
152+
files, that would otherwise be included in every source file.
153+
"""
154+
155+
return self._keep_system_includes
156+
141157
@property
142158
def excludefiles(self) -> List[str]:
143159
return self._excludefiles
@@ -300,6 +316,34 @@ def g(fi: CFile) -> None:
300316

301317
self.iter_files_parallel(g, maxprocesses)
302318

319+
def check_digests(self) -> bool:
320+
for cfile in list(self.cfiles):
321+
for cfun in cfile.get_functions():
322+
if cfun.analysis_digests.is_active:
323+
return True
324+
return False
325+
326+
def outputparameters(self) -> Dict[str, List["CandidateOutputParameter"]]:
327+
result: Dict[str, List["CandidateOutputParameter"]] = {}
328+
for cfile in list(self.cfiles):
329+
for cfun in cfile.get_functions():
330+
result[cfun.name] = cfun.analysis_digests.outputparameters()
331+
return result
332+
333+
def viable_outputparameters(self) -> Dict[str, List["CandidateOutputParameter"]]:
334+
result: Dict[str, List["CandidateOutputParameter"]] = {}
335+
for cfile in list(self.cfiles):
336+
for cfun in cfile.get_functions():
337+
result[cfun.name] = cfun.analysis_digests.viable_outputparameters()
338+
return result
339+
340+
def maybe_outputparameters(self) -> Dict[str, List["CandidateOutputParameter"]]:
341+
result: Dict[str, List["CandidateOutputParameter"]] = {}
342+
for cfile in list(self.cfiles):
343+
for cfun in cfile.get_functions():
344+
result[cfun.name] = cfun.analysis_digests.maybe_outputparameters()
345+
return result
346+
303347
def resolve_vid_function(
304348
self, filevar: FileVarReference) -> Optional["CFunction"]:
305349
"""Returns the function def for the local file-index fid and vid.

chc/app/CAttributes.py

Lines changed: 54 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -113,6 +113,9 @@ def is_index(self) -> bool:
113113
def is_question(self) -> bool:
114114
return False
115115

116+
def accept(self, visitor: "CVisitor") -> None:
117+
raise UF.CHCError("visitor not yet implemented for " + str(self))
118+
116119
def __str__(self) -> str:
117120
return "attrparam:" + self.tags[0]
118121

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

141+
def accept(self, visitor: "CVisitor") -> None:
142+
visitor.visit_attr_int(self)
143+
138144
def __str__(self) -> str:
139145
return "aint(" + str(self.intvalue) + ")"
140146

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

166+
def accept(self, visitor: "CVisitor") -> None:
167+
visitor.visit_attr_str(self)
168+
160169
def __str__(self) -> str:
161170
return "astr(" + str(self.stringvalue) + ")"
162171

@@ -184,6 +193,9 @@ def params(self) -> List[CAttr]:
184193
def is_cons(self) -> bool:
185194
return True
186195

196+
def accept(self, visitor: "CVisitor") -> None:
197+
visitor.visit_attr_cons(self)
198+
187199
def __str__(self) -> str:
188200
return "acons(" + str(self.name) + ")"
189201

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

221+
def accept(self, visitor: "CVisitor") -> None:
222+
visitor.visit_attr_sizeof(self)
223+
209224
def __str__(self) -> str:
210225
return "asizeof(" + str(self.typ) + ")"
211226

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

246+
def accept(self, visitor: "CVisitor") -> None:
247+
visitor.visit_attr_sizeofe(self)
248+
231249
def __str__(self) -> str:
232250
return "asizeofe(" + str(self.param) + ")"
233251

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

271+
def accept(self, visitor: "CVisitor") -> None:
272+
visitor.visit_attr_sizeofs(self)
273+
253274
def __str__(self) -> str:
254275
return "asizeofs(" + str(self.typsig) + ")"
255276

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

296+
def accept(self, visitor: "CVisitor") -> None:
297+
visitor.visit_attr_alignof(self)
298+
275299
def __str__(self) -> str:
276300
return "aalignof(" + str(self.typ) + ")"
277301

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

321+
def accept(self, visitor: "CVisitor") -> None:
322+
visitor.visit_attr_alignofe(self)
323+
297324
def __str__(self) -> str:
298325
return "aalignofe(" + str(self.param) + ")"
299326

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

346+
def accept(self, visitor: "CVisitor") -> None:
347+
visitor.visit_attr_alignofs(self)
348+
319349
def __str__(self) -> str:
320350
return "aalignofs(" + str(self.typsig) + ")"
321351

@@ -343,6 +373,9 @@ def param(self) -> CAttr:
343373
def is_unop(self) -> bool:
344374
return True
345375

376+
def acecpt(self, visitor: "CVisitor") -> None:
377+
visitor.visit_attr_unop(self)
378+
346379
def __str__(self) -> str:
347380
return "aunop(" + self.op + "," + str(self.param) + ")"
348381

@@ -375,6 +408,9 @@ def param2(self) -> CAttr:
375408
def is_binop(self) -> bool:
376409
return True
377410

411+
def accept(self, visitor: "CVisitor") -> None:
412+
visitor.visit_attr_binop(self)
413+
378414
def __str__(self) -> str:
379415
return (
380416
"abinop("
@@ -410,6 +446,9 @@ def param(self) -> CAttr:
410446
def is_dot(self) -> bool:
411447
return True
412448

449+
def accept(self, visitor: "CVisitor") -> None:
450+
visitor.visit_attr_dot(self)
451+
413452
def __str__(self) -> str:
414453
return "adot(" + str(self.param) + "." + self.suffix + ")"
415454

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

478+
def accept(self, visitor: "CVisitor") -> None:
479+
visitor.visit_attr_star(self)
480+
439481
def __str__(self) -> str:
440482
if self.index == self.args[0]:
441483
return "astar()"
@@ -461,6 +503,9 @@ def param(self) -> CAttr:
461503
def is_addrof(self) -> bool:
462504
return True
463505

506+
def accept(self, visitor: "CVisitor") -> None:
507+
visitor.visit_attr_addrof(self)
508+
464509
def __str__(self) -> str:
465510
return "aaddrof(" + str(self.param) + ")"
466511

@@ -488,6 +533,9 @@ def param2(self) -> CAttr:
488533
def is_index(self) -> bool:
489534
return True
490535

536+
def accept(self, visitor: "CVisitor") -> None:
537+
visitor.visit_attr_index(self)
538+
491539
def __str__(self) -> str:
492540
return "aindex(" + str(self.param1) + "," + str(self.param2) + ")"
493541

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

567+
def accept(self, visitor: "CVisitor") -> None:
568+
visitor.visit_attr_question(self)
569+
519570
def __str__(self) -> str:
520571
return (
521572
"aquestion("
@@ -541,6 +592,9 @@ def name(self) -> str:
541592
def params(self) -> List[CAttr]:
542593
return [self.cd.get_attrparam(int(i)) for i in self.args]
543594

595+
def accept(self, visitor: "CVisitor") -> None:
596+
visitor.visit_attribute(self)
597+
544598
def __str__(self) -> str:
545599
return self.name + ": " + ",".join([str(p) for p in self.params])
546600

chc/app/CCompInfo.py

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@
66
#
77
# Copyright (c) 2017-2020 Kestrel Technology LLC
88
# Copyright (c) 2020-2022 Henny B. Sipma
9-
# Copyright (c) 2023-2024 Aarno Labs LLC
9+
# Copyright (c) 2023-2025 Aarno Labs LLC
1010
#
1111
# Permission is hereby granted, free of charge, to any person obtaining a copy
1212
# of this software and associated documentation files (the "Software"), to deal
@@ -39,6 +39,7 @@
3939
from chc.app.CDeclarations import CDeclarations
4040
from chc.app.CFieldInfo import CFieldInfo
4141
from chc.app.CGlobalDeclarations import CGlobalDeclarations
42+
from chc.app.CVisitor import CVisitor
4243

4344

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

104+
def accept(self, visitor: "CVisitor") -> None:
105+
visitor.visit_compinfo(self)
106+
103107
def __str__(self) -> str:
104108
lines = []
105109
lines.append("struct " + self.name)

chc/app/CContextDictionary.py

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -88,6 +88,16 @@ def get_program_context(self, ix: int) -> ProgramContext:
8888
def get_program_context_map(self) -> Dict[int, IndexedTableValue]:
8989
return self.context_table.objectmap(self.get_program_context)
9090

91+
# ----------------- read_xml service ---------------------------------------
92+
93+
def read_xml_program_context(
94+
self, node: ET.Element, tag: str = "ictxt") -> ProgramContext:
95+
xtag = node.get(tag)
96+
if xtag is not None:
97+
return self.get_program_context(int(xtag))
98+
else:
99+
raise UF.CHCError(f"Xml element {node.tag} is missing attribute {tag}")
100+
91101
# ----------------------- Printing -----------------------------------------
92102

93103
def objectmap_to_string(self, name: str) -> str:

chc/app/CDictionary.py

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -268,6 +268,13 @@ def read_xml_exp(self, node: ET.Element, tag: str = "iexp") -> CExp:
268268
else:
269269
raise Exception('xml node was missing the tag "' + tag + '"')
270270

271+
def read_xml_exp_o(
272+
self, node: ET.Element, tag: str = "iexp") -> Optional[CExp]:
273+
xtag_o = node.get(tag)
274+
if xtag_o is not None:
275+
return self.get_exp(int(xtag_o))
276+
return None
277+
271278
def write_xml_exp_opt(
272279
self,
273280
node: ET.Element,

0 commit comments

Comments
 (0)