Skip to content

Commit b99744b

Browse files
sipmasipma
committed
JULIET: add typing
1 parent 72753ed commit b99744b

File tree

4 files changed

+367
-210
lines changed

4 files changed

+367
-210
lines changed

‎chc/cmdline/juliet/JulietTestFileRef.py‎

Lines changed: 188 additions & 141 deletions
Original file line numberDiff line numberDiff line change
@@ -26,194 +26,241 @@
2626
# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
2727
# SOFTWARE.
2828
# ------------------------------------------------------------------------------
29+
"""Juliet scoring reference for a juliet test set file."""
2930

31+
from typing import Any, Dict, List, Optional, TYPE_CHECKING
3032

31-
class JulietTestFileRef:
32-
def __init__(self, testref, d):
33-
self.testref = testref
34-
self.d = d
35-
self.violations = {} # line-no -> JulietViolation
36-
self.safecontrols = {} # line-no -> JulietSafeControl
37-
self.delegated = {}
38-
self.spo_safecontrols = {}
39-
self._initialize()
40-
41-
def get_test(self):
42-
return self.testref.get_test()
43-
44-
def expand(self, m):
45-
return self.testref.expand(m)
46-
47-
def get_violations(self):
48-
return sorted(self.violations.items())
49-
50-
def get_safe_controls(self):
51-
return sorted(self.safecontrols.items())
52-
53-
"""f: (line,julietppo) -> unit. """
54-
55-
def iter(self, f):
56-
self.iter_violations(f)
57-
self.iter_safe_controls(f)
58-
59-
"""f: (line,julietppo) -> unit. """
60-
61-
def iter_violations(self, f):
62-
for (l, vs) in self.get_violations():
63-
for v in vs:
64-
f(l, v)
33+
if TYPE_CHECKING:
34+
from chc.cmdline.juliet.JulietTestRef import JulietTestRef
35+
from chc.proof.CFunctionPO import CFunctionPO
6536

66-
"""f: (line,julietppo) -> unit. """
6737

68-
def iter_safe_controls(self, f):
69-
for (l, ss) in self.get_safe_controls():
70-
for s in ss:
71-
f(l, s)
38+
class JulietTestFileRef:
7239

73-
def __str__(self):
74-
lines = []
40+
def __init__(
41+
self,
42+
testref: "JulietTestRef",
43+
test: str,
44+
d: Dict[str, Any]) -> None:
45+
self._testref = testref
46+
self._test: str
47+
self._d = d
48+
self._violations: Optional[Dict[int, List[JulietViolation]]] = None
49+
self._safecontrols: Optional[Dict[int, List[JulietSafeControl]]] = None
50+
51+
@property
52+
def testref(self) -> "JulietTestRef":
53+
return self._testref
54+
55+
@property
56+
def test(self) -> str:
57+
return self._test
58+
59+
@property
60+
def violations(self) -> Dict[int, List[JulietViolation]]:
61+
if self._violations is None:
62+
self._violations = {}
63+
for line in self._d["violations"]:
64+
self._violations[int(line)] = []
65+
for v in self._d["violations"][line]:
66+
ppovs = self.expand(v)
67+
for ppov in ppovs:
68+
self._violations[int(line)].append(
69+
JulietViolation(self, self.test, int(line), ppov))
70+
return self._violations
71+
72+
@property
73+
def safe_controls(self) -> Dict[int, List[JulietSafeControl]]:
74+
if self._safecontrols is None:
75+
self._safecontrols = {}
76+
for line in self._d["safe-controls"]:
77+
self._safecontrols[int(line)] = []
78+
for s in self._d["safe-controls"][line]:
79+
ppovs = self.expand(s)
80+
for ppov in ppovs:
81+
self._safecontrols[int(line)].append(
82+
JulietSafeControl(self, self.test, int(line), ppov))
83+
return self._safecontrols
84+
85+
def expand(self, m: str) -> List[Dict[str, Any]]:
86+
return self.testref.expand_macro(m)
87+
88+
def get_violations(self) -> List[JulietViolation]:
89+
result: List[JulietViolation] = []
90+
for (line, v) in sorted(self.violations.items()):
91+
result.extend(v)
92+
return result
93+
94+
def get_safe_controls(self) -> List[JulietSafeControl]:
95+
result: List[JulietSafeControl] = []
96+
for (line, s) in sorted(self.safe_controls.items()):
97+
result.extend(s)
98+
return result
99+
100+
def __str__(self) -> str:
101+
lines: List[str] = []
75102
lines.append(" violations:")
76103
for line in self.violations:
77104
lines.append(" line " + str(line))
78105
for v in self.violations[line]:
79106
lines.append(" " + str(v))
80107
lines.append("")
81108
lines.append(" safe-controls:")
82-
for line in self.safecontrols:
109+
for line in self.safe_controls:
83110
lines.append(" line " + str(line))
84-
for s in self.safecontrols[line]:
111+
for s in self.safe_controls[line]:
85112
lines.append(" " + str(s))
86113
return "\n".join(lines)
87114

88-
def _initialize(self):
89-
for line in self.d["violations"]:
90-
self.violations[int(line)] = []
91-
for v in self.d["violations"][line]:
92-
ppovs = self.expand(v)
93-
for ppov in ppovs:
94-
self.violations[int(line)].append(
95-
JulietViolation(self, int(line), ppov)
96-
)
97-
for line in self.d["safe-controls"]:
98-
self.safecontrols[int(line)] = []
99-
for s in self.d["safe-controls"][line]:
100-
pposs = self.expand(s)
101-
for ppos in pposs:
102-
self.safecontrols[int(line)].append(
103-
JulietSafeControl(self, int(line), ppos)
104-
)
105-
106-
107-
class JulietPpo(object):
108-
def __init__(self, testfileref, line, d):
109-
self.testfileref = testfileref
110-
self.line = line
111-
self.predicate = d["P"]
112-
self.predarg = None
113-
self.expctxt = None
114-
self.cfgctxt = None
115-
self.variablename = None
116-
self.variablenameplus = None
117-
self.variablederef = None
118-
self.targettype = None
119-
self.referencetype = None
120-
if "A" in d:
121-
self.predarg = d["A"]
122-
if "E" in d:
123-
self.expctxt = d["E"]
124-
if "C" in d:
125-
self.cfgctxt = d["C"]
126-
if "V" in d:
127-
self.variablename = d["V"]
128-
if "VP" in d:
129-
self.variablenameplus = d["VP"]
130-
if "D" in d:
131-
self.variablederef = d["D"]
132-
if "T" in d:
133-
self.targettype = d["T"]
134-
if "R" in d:
135-
self.referencetype = d["R"]
136-
137-
def get_test(self):
138-
return self.testfileref.get_test()
139-
140-
def has_pred_arg(self):
141-
return not (self.predarg is None)
142-
143-
def has_exp_ctxt(self):
144-
return not (self.expctxt is None)
145-
146-
def has_cfg_ctxt(self):
147-
return not (self.cfgctxt is None)
148-
149-
def has_variable_names(self):
150-
return not (self.variablename is None)
151-
152-
def has_variable_names_plus(self):
153-
return not (self.variablenameplus is None)
154-
155-
def has_variable_deref(self):
156-
return not (self.variablederef is None)
157-
158-
def has_target_type(self):
159-
return not (self.targettype is None)
160-
161-
def has_reference_type(self):
162-
return not (self.referencetype is None)
163-
164-
def matches_pred_arg(self, ppo):
115+
116+
class JulietPpo:
117+
"""Primary proof obligation."""
118+
119+
def __init__(
120+
self,
121+
testfileref: JulietTestFileRef,
122+
test: str,
123+
line: int,
124+
d: Dict[str, Any]) -> None:
125+
self._testfileref = testfileref
126+
self._test = test
127+
self._line = line
128+
self._d = d
129+
130+
@property
131+
def testfileref(self) -> JulietTestFileRef:
132+
return self._testfileref
133+
134+
@property
135+
def test(self) -> str:
136+
return self._test
137+
138+
@property
139+
def line(self) -> int:
140+
return self._line
141+
142+
@property
143+
def predicate(self) -> str:
144+
return self._d["P"]
145+
146+
def has_pred_arg(self) -> bool:
147+
return "A" in self._d
148+
149+
@property
150+
def predarg(self) -> List[str]:
151+
return self._d.get("A", [])
152+
153+
def has_exp_ctxt(self) -> bool:
154+
return "E" in self._d
155+
156+
@property
157+
def expctxt(self) -> str:
158+
return self._d["E"]
159+
160+
def has_cfg_ctxt(self) -> bool:
161+
return "C" in self._d
162+
163+
def has_variable_names(self) -> bool:
164+
return "V" in self._d
165+
166+
@property
167+
def variable_names(self) -> List[str]:
168+
return self._d.get("V", [])
169+
170+
def has_variable_names_plus(self) -> bool:
171+
return "VP" in self._d
172+
173+
@property
174+
def variable_names_plus(self) -> List[str]:
175+
return self._d.get("VP", [])
176+
177+
def has_variable_deref(self) -> bool:
178+
return "D" in self._d
179+
180+
@property
181+
def variable_derefs(self) -> List[str]:
182+
return self._d.get("D", [])
183+
184+
def has_target_type(self) -> bool:
185+
return "T" in self._d
186+
187+
@property
188+
def targettype(self) -> str:
189+
return self._d["T"]
190+
191+
def has_reference_type(self) -> bool:
192+
return "R" in self._d
193+
194+
@property
195+
def reference_type(self) -> str:
196+
return self._d["R"]
197+
198+
def matches_pred_arg(self, ppo: "CFunctionPO") -> bool:
165199
return (not self.has_pred_arg()) or any(
166200
[ppo.has_argument_name(vname) for vname in self.predarg]
167201
)
168202

169-
def matches_exp_ctxt(self, ppo):
203+
def matches_exp_ctxt(self, ppo: "CFunctionPO") -> bool:
170204
return (not self.has_exp_ctxt()) or str(
171-
ppo.context.get_exp_context()
205+
ppo.context.exp_context
172206
) == self.expctxt
173207

174-
def matches_variable_names(self, ppo):
208+
def matches_variable_names(self, ppo: "CFunctionPO") -> bool:
175209
return (not self.has_variable_names()) or any(
176-
[ppo.has_variable_name(vname) for vname in self.variablename]
210+
[ppo.has_variable_name(vname) for vname in self.variable_names]
177211
)
178212

179-
def matches_variable_names_plus(self, ppo):
213+
def matches_variable_names_plus(self, ppo: "CFunctionPO") -> bool:
180214
return (not self.has_variable_names_plus()) or any(
181-
[ppo.has_variable_name_op(vname, "+") for vname in self.variablenameplus]
215+
[ppo.has_variable_name_op(vname, "+")
216+
for vname in self.variable_names_plus]
182217
)
183218

184-
def matches_variable_deref(self, ppo):
219+
def matches_variable_deref(self, ppo: "CFunctionPO") -> bool:
185220
return (not self.has_variable_deref()) or any(
186-
[ppo.has_variable_name_deref(vname) for vname in self.variablederef]
221+
[ppo.has_variable_name_deref(vname)
222+
for vname in self.variable_derefs]
187223
)
188224

189-
def matches_target_type(self, ppo):
190-
return (not self.has_target_type()) or str(
191-
ppo.predicate.get_tgt_kind()
225+
def matches_target_type(self, ppo: "CFunctionPO") -> bool:
226+
return (not self.has_target_type()) or str(ppo.predicate.tgtkind
192227
) == self.targettype
193228

194-
def matches_reference_type(self, ppo):
229+
def matches_reference_type(self, ppo: "CFunctionPO") -> bool:
195230
return (not self.has_reference_type()) or (
196-
self.referencetype == "mem" and ppo.predicate.has_ref_type()
231+
self.reference_type == "mem" and ppo.predicate.has_ref_type()
197232
)
198233

199-
def __str__(self):
234+
def __str__(self) -> str:
200235
ctxt = ""
201236
if self.has_exp_ctxt():
202-
ctxt = " (" + self.get_exp_ctxt() + ")"
237+
ctxt = " (" + self.expctxt + ")"
203238
return str(self.line) + " " + self.predicate + ctxt
204239

205240

206241
class JulietViolation(JulietPpo):
207-
def __init__(self, testfileref, line, d):
208-
JulietPpo.__init__(self, testfileref, line, d)
209242

210-
def is_violation(self):
243+
def __init__(
244+
self,
245+
testfileref: JulietTestFileRef,
246+
test: str,
247+
line: int,
248+
d: Dict[str, Any]) -> None:
249+
JulietPpo.__init__(self, testfileref, test, line, d)
250+
251+
def is_violation(self) -> bool:
211252
return True
212253

213254

214255
class JulietSafeControl(JulietPpo):
215-
def __init__(self, testfileref, line, d):
216-
JulietPpo.__init__(self, testfileref, line, d)
217256

218-
def is_violation(self):
257+
def __init__(
258+
self,
259+
testfileref: JulietTestFileRef,
260+
test: str,
261+
line: int,
262+
d: Dict[str, Any]) -> None:
263+
JulietPpo.__init__(self, testfileref, test, line, d)
264+
265+
def is_violation(self) -> bool:
219266
return False

0 commit comments

Comments
 (0)