kmax
kmax copied to clipboard
krepair Z3Exception: invalid declaration, constant already declared
For a patch in Linux kernel x86_64 v5.13 patches, krepair terminates due to a z3 failure. Here is the error message (tail of klocalizer stderr):
DEBUG: SuperC config creation diagnostic info was written to files.
Traceback (most recent call last):
File "/data1/paul/kmax/kmax_env/bin/klocalizer", line 1575, in <module>
klocalizerCLI()
File "/data1/paul/kmax/kmax_env/bin/klocalizer", line 1068, in klocalizerCLI
get_presence_conditions(unit2srcfile(unit), arch)
File "/data1/paul/kmax/kmax_env/bin/klocalizer", line 811, in get_presence_conditions
cb = superc.get_pc(srcfile, arch, linux_ksrc, superc_formulas_dir, superc_timeout, logger)
File "/data1/paul/kmax/kmax_env/lib/python3.8/site-packages/kmax/superc.py", line 307, in get_pc
pc = Klocalizer.ConditionalBlock._ConditionalBlock__parse_cb(literal_eval(superc_pcfile_content))
File "/data1/paul/kmax/kmax_env/lib/python3.8/site-packages/kmax/klocalizer.py", line 890, in __parse_cb
cb.sub_block_groups = Klocalizer.ConditionalBlock.__parse_sub(cb_string_rep["Sub"], cb)
File "/data1/paul/kmax/kmax_env/lib/python3.8/site-packages/kmax/klocalizer.py", line 864, in __parse_sub
cb = Klocalizer.ConditionalBlock._ConditionalBlock__parse_cb(cb_str)
File "/data1/paul/kmax/kmax_env/lib/python3.8/site-packages/kmax/klocalizer.py", line 888, in __parse_cb
z3_solver.from_string(pc_string) # TODO: make this an expression instead?
File "/data1/paul/kmax/kmax_env/lib/python3.8/site-packages/z3_solver-4.8.14.0-py3.8-linux-x86_64.egg/z3/z3.py", line 7115, in from_string
Z3_solver_from_string(self.ctx.ref(), self.solver, s)
File "/data1/paul/kmax/kmax_env/lib/python3.8/site-packages/z3_solver-4.8.14.0-py3.8-linux-x86_64.egg/z3/z3core.py", line 3871, in Z3_solver_from_string
_elems.Check(a0)
File "/data1/paul/kmax/kmax_env/lib/python3.8/site-packages/z3_solver-4.8.14.0-py3.8-linux-x86_64.egg/z3/z3core.py", line 1447, in Check
raise self.Exception(self.get_error_message(ctx, err))
z3.z3types.Z3Exception: b'(error "line 13 column 39: invalid declaration, constant \'CONFIG_NODES_SHIFT\' (with the given signature) already declared")\n'
Here is the list of (patch, builtin config file) pairs (all belong to the same patch):
3931-c244297acbe5/allyesconfig
3931-c244297acbe5/defconfig
3931-c244297acbe5/randconfig