Skip to content

Commit 8b558bb

Browse files
sipmasipma
committed
INV: add objectmaps for table output
1 parent 50b89c6 commit 8b558bb

17 files changed

+191
-52
lines changed

‎chc/invariants/CFunDictionaryRecord.py‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@
44
# ------------------------------------------------------------------------------
55
# The MIT License (MIT)
66
#
7-
# Copyright (c) 2023 Aarno Labs LLC
7+
# Copyright (c) 2023-2024 Aarno Labs LLC
88
#
99
# Permission is hereby granted, free of charge, to any person obtaining a copy
1010
# of this software and associated documentation files (the "Software"), to deal

‎chc/invariants/CFunInvDictionary.py‎

Lines changed: 30 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@
55
# The MIT License (MIT)
66
#
77
# Copyright (c) 2017-2020 Kestrel Technology LLC
8-
# Copyright (c) 2020-2022 Henny Sipma
8+
# Copyright (c) 2020-2022 Henny B. Sipma
99
# Copyright (c) 2023-2024 Aarno Labs LLC
1010
#
1111
# Permission is hereby granted, free of charge, to any person obtaining a copy
@@ -26,10 +26,11 @@
2626
# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
2727
# SOFTWARE.
2828
# ------------------------------------------------------------------------------
29+
"""Dictionary of indexed function invariants."""
2930

3031
import xml.etree.ElementTree as ET
3132

32-
from typing import List, TYPE_CHECKING
33+
from typing import Callable, Dict, List, Mapping, TYPE_CHECKING
3334

3435
from chc.invariants.CFunDictionaryRecord import invregistry
3536
from chc.invariants.CInvariantFact import CInvariantFact
@@ -59,6 +60,11 @@ def __init__(self, cfun: "CFunction", xnode: ET.Element) -> None:
5960
self.invariant_fact_table,
6061
# self.invariant_list_table
6162
]
63+
self._objmaps: Dict[
64+
str, Callable[[], Mapping[int, IT.IndexedTableValue]]] = {
65+
"nrv": self.get_non_relational_value_map,
66+
"invfact": self.get_invariant_fact_map
67+
}
6268
self.initialize(xnode)
6369

6470
@property
@@ -85,12 +91,19 @@ def get_non_relational_value(self, ix: int) -> CNonRelationalValue:
8591
self.non_relational_value_table.retrieve(ix),
8692
CNonRelationalValue)
8793

94+
def get_non_relational_value_map(self) -> Dict[int, IT.IndexedTableValue]:
95+
return self.non_relational_value_table.objectmap(
96+
self.get_non_relational_value)
97+
8898
def get_invariant_fact(self, ix: int) -> CInvariantFact:
8999
return invregistry.mk_instance(
90100
self,
91101
self.invariant_fact_table.retrieve(ix),
92102
CInvariantFact)
93103

104+
def get_invariant_fact_map(self) -> Dict[int, IT.IndexedTableValue]:
105+
return self.invariant_fact_table.objectmap(self.get_invariant_fact)
106+
94107
# ------------------- Provide read_xml service ---------------------------
95108

96109
# TBD
@@ -113,6 +126,21 @@ def initialize(self, xnode: ET.Element) -> None:
113126

114127
# ---------------------- Printing ----------------------------------------
115128

129+
def objectmap_to_string(self, name: str) -> str:
130+
if name in self._objmaps:
131+
objmap = self._objmaps[name]()
132+
lines: List[str] = []
133+
if len(objmap) == 0:
134+
lines.append("\nTable for {name} is empty\n")
135+
else:
136+
lines.append("index value")
137+
lines.append("-" * 80)
138+
for (ix, obj) in objmap.items():
139+
lines.append(str(ix).rjust(3) + " " + str(obj))
140+
return "\n".join(lines)
141+
else:
142+
raise UF.CHCError(f"Name: {name} does not correspond to a table")
143+
116144
def __str__(self) -> str:
117145
lines: List[str] = []
118146
for t in self.tables:

‎chc/invariants/CFunInvariantTable.py‎

Lines changed: 5 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -5,8 +5,8 @@
55
# The MIT License (MIT)
66
#
77
# Copyright (c) 2017-2020 Kestrel Technology LLC
8-
# Copyright (c) 2020-2022 Henny Sipma
9-
# Copyright (c) 2023 Aarno Labs LLC
8+
# Copyright (c) 2020-2022 Henny B. Sipma
9+
# Copyright (c) 2023-2024 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
@@ -26,6 +26,7 @@
2626
# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
2727
# SOFTWARE.
2828
# ------------------------------------------------------------------------------
29+
"""Table of invariant facts for an individual function."""
2930

3031
import xml.etree.ElementTree as ET
3132

@@ -95,7 +96,8 @@ def invariants(self) -> Dict[int, List[CInvariantFact]]:
9596
self.invd.get_invariant_fact(findex))
9697
return self._invariants
9798

98-
def context_invariants(self, context: "ProgramContext") -> List[CInvariantFact]:
99+
def context_invariants(
100+
self, context: "ProgramContext") -> List[CInvariantFact]:
99101
ictxt = self.ctxtd.index_cfg_projection(context)
100102
if ictxt in self.invariants:
101103
return self.invariants[ictxt]
@@ -173,13 +175,3 @@ def __str__(self) -> str:
173175
for inv in invs:
174176
lines.append(" " + str(inv))
175177
return "\n".join(lines)
176-
177-
'''
178-
def _read_xml(self, xnode):
179-
for xloc in xnode.findall("loc"):
180-
ictxt = int(xloc.get("ictxt"))
181-
self.invariants[ictxt] = []
182-
if "ifacts" in xloc.attrib:
183-
for findex in [int(x) for x in xloc.get("ifacts").split(",")]:
184-
self.invariants[ictxt].append(self.invd.get_invariant_fact(findex))
185-
'''

‎chc/invariants/CFunVarDictionary.py‎

Lines changed: 9 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -5,8 +5,8 @@
55
# The MIT License (MIT)
66
#
77
# Copyright (c) 2017-2020 Kestrel Technology LLC
8-
# Copyright (c) 2020-2022 Henny Sipma
9-
# Copyright (c) 2023 Aarno Labs LLC
8+
# Copyright (c) 2020-2022 Henny B. Sipma
9+
# Copyright (c) 2023-2024 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
@@ -26,6 +26,7 @@
2626
# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
2727
# SOFTWARE.
2828
# ------------------------------------------------------------------------------
29+
"""Dictionary of indexed variables for an individual function."""
2930

3031
import os
3132

@@ -73,7 +74,8 @@ def __init__(self, cfun: "CFunction", xnode: ET.Element) -> None:
7374
self.memory_reference_data_table,
7475
self.constant_value_variable_table,
7576
self.c_variable_denotation_table]
76-
self._objmaps: Dict[str, Callable[[], Mapping[int, IndexedTableValue]]] = {
77+
self._objmaps: Dict[
78+
str, Callable[[], Mapping[int, IndexedTableValue]]] = {
7779
"membase": self.get_memory_base_map,
7880
"memref": self.get_memory_reference_data_map,
7981
"cvv": self.get_constant_value_variable_map,
@@ -190,10 +192,12 @@ def objectmap_to_string(self, name: str) -> str:
190192
objmap = self._objmaps[name]()
191193
lines: List[str] = []
192194
if len(objmap) == 0:
193-
lines.append("Table is empty")
195+
lines.append(f"\nTable for {name} is empty")
194196
else:
197+
lines.append("index value")
198+
lines.append("-" * 80)
195199
for (ix, obj) in objmap.items():
196-
lines.append(str(ix).rjust(3) + " " + str(obj))
200+
lines.append(str(ix).rjust(3) + " " + str(obj))
197201
return "\n".join(lines)
198202
else:
199203
raise UF.CHCError(

‎chc/invariants/CFunXprDictionary.py‎

Lines changed: 50 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -5,8 +5,8 @@
55
# The MIT License (MIT)
66
#
77
# Copyright (c) 2017-2020 Kestrel Technology LLC
8-
# Copyright (c) 2020-2022 Henny Sipma
9-
# Copyright (c) 2023 Aarno Labs LLC
8+
# Copyright (c) 2020-2022 Henny B. Sipma
9+
# Copyright (c) 2023-2024 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
@@ -26,14 +26,16 @@
2626
# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
2727
# SOFTWARE.
2828
# ------------------------------------------------------------------------------
29+
"""Dictionary of indexed expressions for an individual function."""
2930

3031
import os
3132

3233
import xml.etree.ElementTree as ET
3334

34-
from typing import List, TYPE_CHECKING
35+
from typing import Callable, Dict, List, Mapping, TYPE_CHECKING
3536

3637
import chc.util.fileutil as UF
38+
from chc.util.IndexedTable import IndexedTableValue
3739
import chc.util.IndexedTable as IT
3840

3941
from chc.invariants.CFunDictionaryRecord import xprregistry
@@ -71,6 +73,15 @@ def __init__(self, vd: "CFunVarDictionary", xnode: ET.Element) -> None:
7173
self.xpr_list_table,
7274
self.xpr_list_list_table
7375
]
76+
self._objmaps: Dict[
77+
str, Callable[[], Mapping[int, IndexedTableValue]]] = {
78+
"numerical": self.get_numerical_map,
79+
"symbol": self.get_symbol_map,
80+
"variable": self.get_variable_map,
81+
"xcst": self.get_xcst_map,
82+
"xpr": self.get_xpr_map,
83+
"xprlist": self.get_xpr_list_map,
84+
"xprlistlist": self.get_xpr_list_list_map}
7485
self.initialize(xnode)
7586

7687
@property
@@ -85,18 +96,27 @@ def get_numerical(self, ix: int) -> CXNumerical:
8596
else:
8697
raise UF.CHCError("Illegal numerical index value: " + str(ix))
8798

99+
def get_numerical_map(self) -> Dict[int, IndexedTableValue]:
100+
return self.numerical_table.objectmap(self.get_numerical)
101+
88102
def get_symbol(self, ix: int) -> CXSymbol:
89103
if ix > 0:
90104
return CXSymbol(self, self.symbol_table.retrieve(ix))
91105
else:
92106
raise UF.CHCError("Illegal symbol index value: " + str(ix))
93107

108+
def get_symbol_map(self) -> Dict[int, IndexedTableValue]:
109+
return self.symbol_table.objectmap(self.get_symbol)
110+
94111
def get_variable(self, ix: int) -> CXVariable:
95112
if ix > 0:
96113
return CXVariable(self, self.variable_table.retrieve(ix))
97114
else:
98115
raise UF.CHCError("Illegal variable index value: " + str(ix))
99116

117+
def get_variable_map(self) -> Dict[int, IndexedTableValue]:
118+
return self.variable_table.objectmap(self.get_variable)
119+
100120
def get_xcst(self, ix: int) -> CXConstant:
101121
if ix > 0:
102122
return xprregistry.mk_instance(
@@ -106,6 +126,9 @@ def get_xcst(self, ix: int) -> CXConstant:
106126
else:
107127
raise UF.CHCError("Illegal constant index value: " + str(ix))
108128

129+
def get_xcst_map(self) -> Dict[int, IndexedTableValue]:
130+
return self.xcst_table.objectmap(self.get_xcst)
131+
109132
def get_xpr(self, ix: int) -> CXXpr:
110133
if ix > 0:
111134
return xprregistry.mk_instance(
@@ -115,18 +138,27 @@ def get_xpr(self, ix: int) -> CXXpr:
115138
else:
116139
raise UF.CHCError("Illegal xpr index value: " + str(ix))
117140

141+
def get_xpr_map(self) -> Dict[int, IndexedTableValue]:
142+
return self.xpr_table.objectmap(self.get_xpr)
143+
118144
def get_xpr_list(self, ix: int) -> CXprList:
119145
if ix > 0:
120146
return CXprList(self, self.xpr_list_table.retrieve(ix))
121147
else:
122148
raise UF.CHCError("Illegal xpr-list index value: " + str(ix))
123149

150+
def get_xpr_list_map(self) -> Dict[int, IndexedTableValue]:
151+
return self.xpr_list_table.objectmap(self.get_xpr_list)
152+
124153
def get_xpr_list_list(self, ix: int) -> CXprListList:
125154
if ix > 0:
126155
return CXprListList(self, self.xpr_list_list_table.retrieve(ix))
127156
else:
128157
raise UF.CHCError("Illegal xpr-list-list index value: " + str(ix))
129158

159+
def get_xpr_list_list_map(self) -> Dict[int, IndexedTableValue]:
160+
return self.xpr_list_list_table.objectmap(self.get_xpr_list_list)
161+
130162
# ------------ Provide read_xml service ----------------------------------
131163

132164
# TBD
@@ -149,6 +181,21 @@ def initialize(self, xnode: ET.Element, force: bool = False) -> None:
149181

150182
# ------------------ Printing --------------------------------------------
151183

184+
def objectmap_to_string(self, name: str) -> str:
185+
if name in self._objmaps:
186+
objmap = self._objmaps[name]()
187+
lines: List[str] = []
188+
if len(objmap) == 0:
189+
lines.append(f"\nTable for {name} is empty\n")
190+
else:
191+
lines.append("index value")
192+
lines.append("-" * 80)
193+
for (ix, obj) in objmap.items():
194+
lines.append(str(ix).rjust(3) + " " + str(obj))
195+
return "\n".join(lines)
196+
else:
197+
raise UF.CHCError(f"Name: {name} does not correspond to a table")
198+
152199
def __str__(self) -> str:
153200
lines: List[str] = []
154201
for t in self.tables:

‎chc/invariants/CInvariantFact.py‎

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -5,8 +5,8 @@
55
# The MIT License (MIT)
66
#
77
# Copyright (c) 2017-2020 Kestrel Technology LLC
8-
# Copyright (c) 2020-2022 Henny Sipma
9-
# Copyright (c) 2023 Aarno Labs LLC
8+
# Copyright (c) 2020-2022 Henny B. Sipma
9+
# Copyright (c) 2023-2024 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
@@ -26,7 +26,7 @@
2626
# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
2727
# SOFTWARE.
2828
# ------------------------------------------------------------------------------
29-
29+
"""Different types of invariants."""
3030

3131
from typing import Any, Dict, List, Optional, TYPE_CHECKING
3232

@@ -64,6 +64,7 @@ def __str__(self) -> str:
6464

6565
@invregistry.register_tag("nrv", CInvariantFact)
6666
class CInvariantNRVFact(CInvariantFact):
67+
"""Non-relational-value fact (relation with symbolic constants)."""
6768

6869
def __init__(
6970
self, invd: "CFunInvDictionary", ixval: IndexedTableValue) -> None:
@@ -105,6 +106,7 @@ def __str__(self) -> str:
105106

106107
@invregistry.register_tag("x", CInvariantFact)
107108
class CUnreachableFact(CInvariantFact):
109+
"""Domain that signals unreachability."""
108110

109111
def __init__(
110112
self, invd: "CFunInvDictionary", ixval: IndexedTableValue) -> None:

0 commit comments

Comments
 (0)