Summary

When initially testing #276, I found that I had run into another, unrelated bug caused by another commit in the commit range I had used.
I wanted to find out whether the cause of the bug was due to my proposed change or simply due to another case that kmax currently does not account for. To do this, I narrowed down the file that the issue occurred at and found the commit that accessed the file drivers/net/ethernet/i825xx/sun3_82586.c.
- The commit in particular is 4bea747f3fbec33c16d369b2f51e55981d7c78d0.
- I applied this commit on kmax4.8-rc4 directly from the Git repository and found that the issue still occurred, marking it an existing issue with kmax and not an issue with my fix.
The issue stems from how kmax handles tagging directives when adding them to a stack (or "conditional block" of directives), as it currently falsely claims that an if directive isn't an if directive simply because it does not have a space between it and the condition.

Steps to reproduce

Steps followed

Clone the Linux kernel and cd into the new directory.
Checkout commit 4bea747f3fbec33c16d369b2f51e55981d7c78d0 with git checkout 4bea747f3fbec33c16d369b2f51e55981d7c78d0.
Get the diff with git show > 4bea747f3fbec33c16d369b2f51e55981d7c78d0.diff.
Get allnoconfig with make.cross ARCH=x86_64 allnoconfig.
Repair the newly-created configuration with klocalizer --repair .config -a x86_64 --include-mutex 4bea747f3fbec33c16d369b2f51e55981d7c78d0.diff.

What I expected to happen

I expected the klocalizer command to complete without any errors, creating a new repaired configuration file that applies constraints from the diff.

What actually happened

I observed the following error:

(kmaxtemp) alexei@turing:~/LinuxKernels/TesterKernels/linux$ klocalizer --repair .config -a x86_64 --include-mutex 4bea747f3fbec33c16d369b2f51e55981d7c78d0.diff
klocalizer, kmax 4.8-rc4
INFO: Diff file was given as input ("4bea747f3fbec33c16d369b2f51e55981d7c78d0.diff"): assuming it was applied to the Linux source.
WARNING: No cached formulas for ae2d37861ddd available for download :(
Traceback (most recent call last):
File "/home/alexei/LinuxKernels/TesterKernels/kmaxtemp/bin/klocalizer", line 1726, in <module>
klocalizerCLI()
File "/home/alexei/LinuxKernels/TesterKernels/kmaxtemp/bin/klocalizer", line 813, in klocalizerCLI
root_cb = SyntaxAnalysis.get_conditional_blocks_of_file(srcfile_fullpath)
File "/home/alexei/LinuxKernels/TesterKernels/kmaxtemp/lib/python3.8/site-packages/kmax/superc.py", line 762, in get_conditional_blocks_of_file
cb = SyntaxAnalysis.get_conditional_blocks(content, line_count)
File "/home/alexei/LinuxKernels/TesterKernels/kmaxtemp/lib/python3.8/site-packages/kmax/superc.py", line 714, in get_conditional_blocks
stack[-1].sub_block_groups.append([new_cb])
IndexError: list index out of range

Additional information:

I entered my own copy of the code and added some debugging statements:

    for linenum in categorized_tokens:
      for i, token_to_type in enumerate(categorized_tokens[linenum]):
        # Get the token and its type
        assert len(token_to_type) == 1 #< One token mapped to its type.
        token = list(token_to_type.keys())[0]
        token_type = token_to_type[token]

        # Check if it is a conditional preprocessor directive
        if token == '#' and token_type == 'preprocessor':
          # Beginning of a new preprocessor directive, read the next token
          # to see if it is a conditional preprocessor directive.
          # Assumption: preprocessor directives like #if are not broken into
          # two lines right after the # sign (# \ if).

          # this code basically gets the next token and then checks if it's an if statement, if it is then it'll create a new conditional block and then add it to thestack
          next_token_to_type = categorized_tokens[linenum][i + 1]
          assert len(next_token_to_type) == 1
          next_token = list(next_token_to_type.keys())[0]
          print(f"DEBUG: processing next_token {next_token} at line {linenum}")
          next_token_type = next_token_to_type[next_token]
          assert next_token_type == "preprocessor"
          if next_token not in ['if', 'ifdef', 'ifndef', 'elif', 'else', 'endif']:
            print(f"DEBUG: next_token not a preprocessor directive, skipping")
            # Not a conditional preprocessor directive
            continue

          if next_token in ['if', 'ifdef', 'ifndef']:
            print(f"DEBUG: next_token is an if directive, opening new block for tkn {next_token} line {linenum}")
            # Open a new conditional block
            new_cb = SyntaxAnalysis.ConditionalBlock()
            new_cb.start_line = linenum
            print(f"DEBUG: current top of stack is {stack[-1]}")
            stack[-1].sub_block_groups.append([new_cb])  # add new block as nested sub-block within current block
            stack.append(new_cb) # focus on new block
            print(f"DEBUG: stack after push: {stack}")
          elif next_token in ['elif', 'else']:
            print(f"DEBUG: next_token is an else/else if directive, tkn {next_token} line {linenum}")
            # Close the currently open conditional block.
            last_cb = stack[-1]
            last_cb.end_line = linenum
            stack.pop()
            print(f"DEBUG: stack after pop: {stack}")

            # Open a new one in the same block group as the closed one.
            new_cb = SyntaxAnalysis.ConditionalBlock()
            new_cb.start_line = linenum
            parent_cb = stack[-1] if stack else None

            print(f"DEBUG: adding new block to parent {parent_cb}")
            parent_cb.sub_block_groups[-1].append(new_cb)
            stack.append(new_cb)
            print(f"DEBUG: stack after push: {stack}")
          elif next_token == 'endif':
            # Close the currently open conditional block.
            print(f"DEBUG: processing 'endif' at line {linenum}")
            last_cb = stack[-1]
            last_cb.end_line = linenum
            stack.pop()
            print(f"DEBUG: stack after pop: {stack}")
          else:
            assert False

    # There must remain only one element, which is the dummy root
    assert len(stack) == 1
    return stack[0]

I found the following:

DEBUG: stack after pop: [<kmax.superc.SyntaxAnalysis.ConditionalBlock object at 0x7f18f7e90970>]
DEBUG: processing next_token ifdef at line 988
DEBUG: next_token is an if directive, opening new block for tkn ifdef line 988
DEBUG: current top of stack is <kmax.superc.SyntaxAnalysis.ConditionalBlock object at 0x7f18f7e90970>
DEBUG: stack after push: [<kmax.superc.SyntaxAnalysis.ConditionalBlock object at 0x7f18f7e90970>, <kmax.superc.SyntaxAnalysis.ConditionalBlock object at 0x7f18f7e52f70>]
DEBUG: processing next_token endif at line 992
DEBUG: processing 'endif' at line 992
DEBUG: stack after pop: [<kmax.superc.SyntaxAnalysis.ConditionalBlock object at 0x7f18f7e90970>]
DEBUG: processing next_token ifndef at line 1007
DEBUG: next_token is an if directive, opening new block for tkn ifndef line 1007
DEBUG: current top of stack is <kmax.superc.SyntaxAnalysis.ConditionalBlock object at 0x7f18f7e90970>
DEBUG: stack after push: [<kmax.superc.SyntaxAnalysis.ConditionalBlock object at 0x7f18f7e90970>, <kmax.superc.SyntaxAnalysis.ConditionalBlock object at 0x7f18f7e52fd0>]
DEBUG: processing next_token endif at line 1009
DEBUG: processing 'endif' at line 1009
DEBUG: stack after pop: [<kmax.superc.SyntaxAnalysis.ConditionalBlock object at 0x7f18f7e90970>]
DEBUG: processing next_token if(NUM_XMIT_BUFFS at line 1020  # PROBLEMATIC LINE
DEBUG: next_token not a preprocessor directive, skipping  # CONSIDERED "NOT A PREPROCESSOR DIRECTIVE"
DEBUG: processing next_token endif at line 1026
DEBUG: processing 'endif' at line 1026
DEBUG: stack after pop: []  # NOTICE STACK
DEBUG: processing next_token if at line 1036
DEBUG: next_token is an if directive, opening new block for tkn if line 1036
Traceback (most recent call last):
File "/home/alexei/IDEProjects/PyCharmProjects/kmax/venv/bin/klocalizer", line 7, in <module>
exec(compile(f.read(), __file__, 'exec'))
File "/home/alexei/IDEProjects/PyCharmProjects/kmax/kmax/klocalizer", line 1728, in <module>
klocalizerCLI()
File "/home/alexei/IDEProjects/PyCharmProjects/kmax/kmax/klocalizer", line 815, in klocalizerCLI
root_cb = SyntaxAnalysis.get_conditional_blocks_of_file(srcfile_fullpath)
File "/home/alexei/IDEProjects/PyCharmProjects/kmax/kmax/superc.py", line 790, in get_conditional_blocks_of_file
cb = SyntaxAnalysis.get_conditional_blocks(content, line_count)
File "/home/alexei/IDEProjects/PyCharmProjects/kmax/kmax/superc.py", line 726, in get_conditional_blocks
stack[-1].sub_block_groups.append([new_cb])  # add new block as nested sub-block within current block
IndexError: list index out of range

Note my comments -- it's clear that the token that processes the if condition with no space is considered "not a preprocessor directive," which later causes an error in the stack.

This is further supported when looking at the Linux kernel code at drivers/net/ethernet/i825xx/sun3_82586.c:


#ifndef NO_NOPCOMMANDS
int next_nop;
#endif
struct priv *p = netdev_priv(dev);

if(skb->len > XMIT_BUFF_SIZE)
{
    printk("%s: Sorry, max. framelength is %d bytes. The length of your frame is %d bytes.\n",dev->name,XMIT_BUFF_SIZE,skb->len);
    return NETDEV_TX_OK;
}

netif_stop_queue(dev);

if(NUM_XMIT_BUFFS > 1) //line 1020

if(test_and_set_bit(0,(void *) &p->lock)) {
    printk("%s: Queue was locked\n",dev->name);
    return NETDEV_TX_BUSY;
}
else

endif

{
    len = skb->len;
    if (len < ETH_ZLEN) {
        memset((void *)p->xmit_cbuffs[p->xmit_count], 0,
               ETH_ZLEN);
        len = ETH_ZLEN;
    }
    skb_copy_from_linear_data(skb, (void *)p->xmit_cbuffs[p->xmit_count], skb->len);

if (NUM_XMIT_BUFFS == 1)


* When adding a space between `if` and `(NUM_XMIT_BUFFS > 1)`, the issue disappears and `klocalizer` attempts to compute line presence conditions:

... INFO: Trying the following architectures: x86_64 INFO: Trying "x86_64" INFO: Computing the line presence conditions under x86_64 for the following units: drivers/net/ethernet/i825xx/sun3_82586.o INFO: Computing line presence conditions for "drivers/net/ethernet/i825xx/sun3_82586.c" [STEP 1/3] reading kextract file [STEP 1/3] finished reading kextract file [STEP 2/3] translated 17299/17299 configuration option dependencies [STEP 3/3] converted 17273/17273 constraints to smtlib2 format [STEP 3/3] pickling the map [STEP 3/3] done WARNING: Failed to compute line presence conditions for "drivers/net/ethernet/i825xx/sun3_82586.c": SuperC config generation error INFO: Searching for a constraints model that cover all or part of the constraints ERROR: No satisfying configuration found. (venv) alexei@turing:~/LinuxKernels/TesterKernels/linux$

paulgazz / kmax

C static analysis code fails to consider conditional directives without spaces #277