kmax icon indicating copy to clipboard operation
kmax copied to clipboard

krepair Z3Exception: invalid declaration, constant already declared

Open necipfazil opened this issue 2 years ago • 0 comments

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

necipfazil avatar May 05 '22 11:05 necipfazil