Skip to content

Commit dea753d

Browse files
leventeBajczileventeBajczi
committed
Added copyright notice to files, and requirements.txt
1 parent 67a5d09 commit dea753d

File tree

6 files changed

+345
-58
lines changed

6 files changed

+345
-58
lines changed

‎BaseCHC2C.py

+117-21
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,22 @@
1+
# Copyright ${current_year} Budapest University of Technology and Economics
2+
#
3+
# Licensed under the Apache License, Version 2.0 (the "License");
4+
# you may not use this file except in compliance with the License.
5+
# You may obtain a copy of the License at
6+
#
7+
# http://www.apache.org/licenses/LICENSE-2.0
8+
#
9+
# Unless required by applicable law or agreed to in writing, software
10+
# distributed under the License is distributed on an "AS IS" BASIS,
11+
# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
12+
# See the License for the specific language governing permissions and
13+
# limitations under the License.
14+
#
15+
116
import z3
217
import re
318

19+
420
# As long as the CHC is nonrecursive, this can be used
521
class BaseCHC2C:
622

@@ -21,44 +37,124 @@ def expr_to_c(self, expr, bound_vars):
2137
if idx < len(bound_vars):
2238
return self.sanitize_identifier(bound_vars[idx][0])
2339
else:
24-
raise ValueError(f"Variable index {idx} out of bounds for bound variables {bound_vars}")
40+
raise ValueError(
41+
f"Variable index {idx} out of bounds for bound variables {bound_vars}"
42+
)
2543
elif z3.is_add(expr):
26-
return '(' + ' + '.join(self.expr_to_c(arg, bound_vars) for arg in expr.children()) + ')'
44+
return (
45+
"("
46+
+ " + ".join(self.expr_to_c(arg, bound_vars) for arg in expr.children())
47+
+ ")"
48+
)
2749
elif z3.is_sub(expr):
28-
return '(' + ' - '.join(self.expr_to_c(arg, bound_vars) for arg in expr.children()) + ')'
50+
return (
51+
"("
52+
+ " - ".join(self.expr_to_c(arg, bound_vars) for arg in expr.children())
53+
+ ")"
54+
)
2955
elif z3.is_mul(expr):
30-
return '(' + ' * '.join(self.expr_to_c(arg, bound_vars) for arg in expr.children()) + ')'
56+
return (
57+
"("
58+
+ " * ".join(self.expr_to_c(arg, bound_vars) for arg in expr.children())
59+
+ ")"
60+
)
3161
elif z3.is_div(expr):
32-
return '(' + ' / '.join(self.expr_to_c(arg, bound_vars) for arg in expr.children()) + ')'
62+
return (
63+
"("
64+
+ " / ".join(self.expr_to_c(arg, bound_vars) for arg in expr.children())
65+
+ ")"
66+
)
3367
elif z3.is_eq(expr):
34-
return '(' + self.expr_to_c(expr.arg(0), bound_vars) + ' == ' + self.expr_to_c(expr.arg(1), bound_vars) + ')'
68+
return (
69+
"("
70+
+ self.expr_to_c(expr.arg(0), bound_vars)
71+
+ " == "
72+
+ self.expr_to_c(expr.arg(1), bound_vars)
73+
+ ")"
74+
)
3575
elif z3.is_le(expr):
36-
return '(' + self.expr_to_c(expr.arg(0), bound_vars) + ' <= ' + self.expr_to_c(expr.arg(1), bound_vars) + ')'
76+
return (
77+
"("
78+
+ self.expr_to_c(expr.arg(0), bound_vars)
79+
+ " <= "
80+
+ self.expr_to_c(expr.arg(1), bound_vars)
81+
+ ")"
82+
)
3783
elif z3.is_ge(expr):
38-
return '(' + self.expr_to_c(expr.arg(0), bound_vars) + ' >= ' + self.expr_to_c(expr.arg(1), bound_vars) + ')'
84+
return (
85+
"("
86+
+ self.expr_to_c(expr.arg(0), bound_vars)
87+
+ " >= "
88+
+ self.expr_to_c(expr.arg(1), bound_vars)
89+
+ ")"
90+
)
3991
elif z3.is_lt(expr):
40-
return '(' + self.expr_to_c(expr.arg(0), bound_vars) + ' < ' + self.expr_to_c(expr.arg(1), bound_vars) + ')'
92+
return (
93+
"("
94+
+ self.expr_to_c(expr.arg(0), bound_vars)
95+
+ " < "
96+
+ self.expr_to_c(expr.arg(1), bound_vars)
97+
+ ")"
98+
)
4199
elif z3.is_gt(expr):
42-
return '(' + self.expr_to_c(expr.arg(0), bound_vars) + ' > ' + self.expr_to_c(expr.arg(1), bound_vars) + ')'
100+
return (
101+
"("
102+
+ self.expr_to_c(expr.arg(0), bound_vars)
103+
+ " > "
104+
+ self.expr_to_c(expr.arg(1), bound_vars)
105+
+ ")"
106+
)
43107
elif z3.is_and(expr):
44-
return '(' + ' && '.join(self.expr_to_c(arg, bound_vars) for arg in expr.children()) + ')'
108+
return (
109+
"("
110+
+ " && ".join(
111+
self.expr_to_c(arg, bound_vars) for arg in expr.children()
112+
)
113+
+ ")"
114+
)
45115
elif z3.is_or(expr):
46-
return '(' + ' || '.join(self.expr_to_c(arg, bound_vars) for arg in expr.children()) + ')'
116+
return (
117+
"("
118+
+ " || ".join(
119+
self.expr_to_c(arg, bound_vars) for arg in expr.children()
120+
)
121+
+ ")"
122+
)
47123
elif z3.is_not(expr):
48-
return '(!' + self.expr_to_c(expr.arg(0), bound_vars) + ')'
124+
return "(!" + self.expr_to_c(expr.arg(0), bound_vars) + ")"
49125
elif z3.is_mod(expr):
50126
# TODO: exact mod behavior
51-
return '(' + self.expr_to_c(expr.arg(0), bound_vars) + ' % ' + self.expr_to_c(expr.arg(1), bound_vars) + ')'
127+
return (
128+
"("
129+
+ self.expr_to_c(expr.arg(0), bound_vars)
130+
+ " % "
131+
+ self.expr_to_c(expr.arg(1), bound_vars)
132+
+ ")"
133+
)
52134
elif z3.is_app(expr) and expr.decl().kind() == z3.Z3_OP_UNINTERPRETED:
53-
return None # the subclass should handle this
135+
return None # the subclass should handle this
54136
elif z3.is_app(expr):
55137
kind = expr.decl().kind()
56138
if kind == z3.Z3_OP_UMINUS:
57-
return '(-' + self.expr_to_c(expr.arg(0), bound_vars) + ')'
139+
return "(-" + self.expr_to_c(expr.arg(0), bound_vars) + ")"
58140
elif kind == z3.Z3_OP_ITE:
59-
return '(' + self.expr_to_c(expr.arg(0), bound_vars) + ' ? ' + self.expr_to_c(expr.arg(1), bound_vars) + ' : ' + self.expr_to_c(expr.arg(2), bound_vars) + ')'
141+
return (
142+
"("
143+
+ self.expr_to_c(expr.arg(0), bound_vars)
144+
+ " ? "
145+
+ self.expr_to_c(expr.arg(1), bound_vars)
146+
+ " : "
147+
+ self.expr_to_c(expr.arg(2), bound_vars)
148+
+ ")"
149+
)
60150
elif kind == z3.Z3_OP_IDIV:
61-
return '(' + ' / '.join(self.expr_to_c(arg, bound_vars) for arg in expr.children()) + ')'
151+
return (
152+
"("
153+
+ " / ".join(
154+
self.expr_to_c(arg, bound_vars) for arg in expr.children()
155+
)
156+
+ ")"
157+
)
62158
raise NotImplementedError(f"Operator not implemented: {expr.decl()}")
63159

64160
def smt_sort_to_c(self, sort):
@@ -72,7 +168,7 @@ def smt_sort_to_c(self, sort):
72168

73169
def sanitize_identifier(self, identifier):
74170
# Ensure the first character is a letter or underscore.
75-
identifier = re.sub(r'^[^A-Za-z_]', '_', identifier)
171+
identifier = re.sub(r"^[^A-Za-z_]", "_", identifier)
76172
# Replace any character that is not a letter, digit, or underscore.
77-
identifier = re.sub(r'[^A-Za-z0-9_]', '_', identifier)
78-
return identifier
173+
identifier = re.sub(r"[^A-Za-z0-9_]", "_", identifier)
174+
return identifier

‎LinearCHC2C.py

+86-12
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,31 @@
1+
# Copyright ${current_year} Budapest University of Technology and Economics
2+
#
3+
# Licensed under the Apache License, Version 2.0 (the "License");
4+
# you may not use this file except in compliance with the License.
5+
# You may obtain a copy of the License at
6+
#
7+
# http://www.apache.org/licenses/LICENSE-2.0
8+
#
9+
# Unless required by applicable law or agreed to in writing, software
10+
# distributed under the License is distributed on an "AS IS" BASIS,
11+
# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
12+
# See the License for the specific language governing permissions and
13+
# limitations under the License.
14+
#
15+
#
16+
# Licensed under the Apache License, Version 2.0 (the "License");
17+
# you may not use this file except in compliance with the License.
18+
# You may obtain a copy of the License at
19+
#
20+
# http://www.apache.org/licenses/LICENSE-2.0
21+
#
22+
# Unless required by applicable law or agreed to in writing, software
23+
# distributed under the License is distributed on an "AS IS" BASIS,
24+
# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
25+
# See the License for the specific language governing permissions and
26+
# limitations under the License.
27+
#
28+
129
import z3
230
import textwrap
331

@@ -7,6 +35,7 @@
735
class RecursiveException(Exception):
836
pass
937

38+
1039
# As long as the CHC is nonrecursive or linear, this can be used
1140
class LinearCHC2C(BaseCHC2C):
1241

@@ -17,7 +46,11 @@ def __init__(self):
1746
self.current_rule = None
1847

1948
def propagate_callgraph(self, func):
20-
name = self.current_rule.name() if not isinstance(self.current_rule, str) else self.current_rule
49+
name = (
50+
self.current_rule.name()
51+
if not isinstance(self.current_rule, str)
52+
else self.current_rule
53+
)
2154
if name not in self.callgraph:
2255
self.callgraph[name] = set()
2356
self.callgraph[name].add(func.name())
@@ -45,7 +78,14 @@ def expr_to_c(self, expr, bound_vars):
4578
self.propagate_callgraph(func)
4679
self.create_uf_vars(expr)
4780
if expr.num_args() > 0:
48-
return '(' + ' && '.join(f"{self.var_lookup[func][i][0]} == {self.expr_to_c(expr.arg(i), bound_vars)}" for i in range(expr.num_args())) + ')'
81+
return (
82+
"("
83+
+ " && ".join(
84+
f"{self.var_lookup[func][i][0]} == {self.expr_to_c(expr.arg(i), bound_vars)}"
85+
for i in range(expr.num_args())
86+
)
87+
+ ")"
88+
)
4989
else:
5090
return self.var_lookup[func][0][0]
5191
else:
@@ -55,9 +95,14 @@ def create_uf_vars(self, expr):
5595
func = expr.decl()
5696
if func not in self.var_lookup:
5797
if expr.num_args() > 0:
58-
self.var_lookup[func] = [(f"{self.sanitize_identifier(str(func))}_{i}", expr.arg(i).sort()) for i in range(expr.num_args())]
98+
self.var_lookup[func] = [
99+
(f"{self.sanitize_identifier(str(func))}_{i}", expr.arg(i).sort())
100+
for i in range(expr.num_args())
101+
]
59102
else:
60-
self.var_lookup[func] = [(self.sanitize_identifier(str(func)), z3.BoolSort())]
103+
self.var_lookup[func] = [
104+
(self.sanitize_identifier(str(func)), z3.BoolSort())
105+
]
61106

62107
def chc_to_c_program(self, smtlib_file_content, filename):
63108
# Parse the CHCs using Z3
@@ -70,7 +115,13 @@ def chc_to_c_program(self, smtlib_file_content, filename):
70115
# Check if this is a forall with an implication
71116
if z3.is_quantifier(rule) and rule.is_forall():
72117
# Extract variables and body
73-
bound_vars = [(rule.var_name(rule.num_vars() - i - 1), rule.var_sort(rule.num_vars() - i - 1)) for i in range(rule.num_vars())]
118+
bound_vars = [
119+
(
120+
rule.var_name(rule.num_vars() - i - 1),
121+
rule.var_sort(rule.num_vars() - i - 1),
122+
)
123+
for i in range(rule.num_vars())
124+
]
74125
body = rule.body()
75126

76127
if z3.is_implies(body):
@@ -85,27 +136,41 @@ def chc_to_c_program(self, smtlib_file_content, filename):
85136

86137
self.check_nonrecursive()
87138

88-
c_program = textwrap.dedent(f"""
139+
c_program = textwrap.dedent(
140+
f"""
89141
extern int __VERIFIER_nondet_int();
90142
extern _Bool __VERIFIER_nondet__Bool();
91143
extern void abort(void);
92144
extern void __assert_fail(const char *, const char *, unsigned int, const char *);
93145
void reach_error() {{ __assert_fail("0", "{filename}", 0, "reach_error"); }}
94-
""")
146+
"""
147+
)
95148
c_program += "// function declarations\n"
96-
c_program += "\n".join([f"void {func_name}();" for func_name in function_names]) + "\n\n"
149+
c_program += (
150+
"\n".join([f"void {func_name}();" for func_name in function_names]) + "\n\n"
151+
)
97152
c_program += "// global variables\n"
98153
for vars in self.var_lookup.values():
99-
c_program += "\n".join([f"{self.smt_sort_to_c(v[1])} {v[0]};" for v in vars]) + "\n\n"
154+
c_program += (
155+
"\n".join([f"{self.smt_sort_to_c(v[1])} {v[0]};" for v in vars])
156+
+ "\n\n"
157+
)
100158
c_program += "// rules\n"
101159
c_program += "\n".join(functions) + "\n\n"
102160
c_program += "// main function\n"
103161
c_program += "int main() {\n int i = __VERIFIER_nondet_int();\n switch(i) {\n"
104-
c_program += "\n".join([f" case {i}: {func}(); break;" for i, func in enumerate(function_names)]) + "\n"
162+
c_program += (
163+
"\n".join(
164+
[
165+
f" case {i}: {func}(); break;"
166+
for i, func in enumerate(function_names)
167+
]
168+
)
169+
+ "\n"
170+
)
105171
c_program += " default: abort(); break;\n }\n}"
106172
return c_program
107173

108-
109174
def create_function(self, body, bound_vars, func_name, rule):
110175
condition = body.arg(0) # Left-hand side of the implication
111176
conclusion = body.arg(1) # Right-hand side of the implication
@@ -119,7 +184,16 @@ def create_function(self, body, bound_vars, func_name, rule):
119184
# Generate function body
120185
func_body += f"void {func_name}() {{\n"
121186
# Declare the parameters as unbound variables
122-
func_body += " " + "\n ".join(map(lambda v: f"{self.smt_sort_to_c(v[1])} {v[0]} = __VERIFIER_nondet_{self.smt_sort_to_c(v[1])}();", [x for x in bound_vars if x[0] != "CHC_COMP_UNUSED"])) + "\n"
187+
func_body += (
188+
" "
189+
+ "\n ".join(
190+
map(
191+
lambda v: f"{self.smt_sort_to_c(v[1])} {v[0]} = __VERIFIER_nondet_{self.smt_sort_to_c(v[1])}();",
192+
[x for x in bound_vars if x[0] != "CHC_COMP_UNUSED"],
193+
)
194+
)
195+
+ "\n"
196+
)
123197
# Convert the left-hand side of the implication to C (condition)
124198
condition_str = self.expr_to_c(condition, bound_vars)
125199
func_body += f" if ({condition_str}) {{\n"

0 commit comments

Comments
 (0)