Project

General

Profile

Actions

Bug #7998

closed

seq_operations specification: Invalid scenario

Added by Alexey Khoroshilov about 7 years ago. Updated about 7 years ago.

Status:
Closed
Priority:
Urgent
Assignee:
Category:
Environment models
Target version:
-
Start date:
02/24/2017
Due date:
% Done:

0%

Estimated time:
Detected in build:
svn
Platform:
Published in build:

Description

Current state:

      "start_step": {
        "process": "[start].(<start_success>.{next_step} | <start_failed>.[stop].(deregister))" 
      },
      "next_step": {
        "process": "[next].[show].(<next_success>.{next_step} | <next_fail>.[stop].{start_step})" 
      },

while it should be something like this:

    struct seq_file *m = %seq_file%;
    loff_t index = 0;
    void *p;
    p = op->start(m, &index);
check_res_and_show:
    if ((p == NULL) || IS_ERR(p)) goto stop;
    int error = op->show(m, p);
    if (error < 0) goto stop;
    if (nondet_int()) goto stop;
    p = op->next(m, &index);
    goto check_res_and_show;
stop:
    op->stop(m, p);

Actions #1

Updated by Evgeny Novikov about 7 years ago

  • Assignee set to Ilja Zakharov

It is unclear why it is so important in terms of, say, false alarms or/and missed bugs. Any way we have the only developer who can fix this well.

Actions #2

Updated by Ilja Zakharov about 7 years ago

Fixed in seq-ops-fix branch.

To make fixing a bit more straightforward it would be nice to have an example of a false positive to test my fix. Otherwise I do testing using my tests but they contain not many specific checks.

Actions #3

Updated by Ilja Zakharov about 7 years ago

  • Status changed from New to Resolved
Actions #4

Updated by Alexey Khoroshilov about 7 years ago

net/packet/af_packet.ko, generic:memory

Actions #5

Updated by Ilja Zakharov about 7 years ago

  • Status changed from Resolved to Verified

After an additional fix the false positive is gone.

The fixed merged in master in 637453e.

Actions #6

Updated by Ilja Zakharov about 7 years ago

  • Status changed from Verified to Closed
Actions #7

Updated by Alexey Khoroshilov about 7 years ago

  • Status changed from Closed to Open

I have a couple of questions about the implementation.

          "index": {
            "signature": "loff_t *a" 
          }

          "start": {
            "callback": "%ops.start%",
            "parameters": [
              "%seq_file%", "%index%" 
            ],
          },
          "stop": {
            "callback": "%ops.stop%",
            "pre-call": [
              "%seq_file%->index = %index%;" 
            ],
            "post-call": [
              "%seq_file%->index = %index%;" 
            ],
          },

1. Does index passed as argument mean a pointer to exactly one integer?
2. "%seq_file%->index = index;" looks like loff_t* to loff_t assignment. Is it?

Actions #8

Updated by Ilja Zakharov about 7 years ago

  • Status changed from Open to Resolved

1. Does index passed as argument mean a pointer to exactly one integer?

EMG for each label and interface type pair generates a variable. In this case it generates a variable ldv_$num$_index_index which is passed to start and next callbacks. So if it is not changed by callbacks, then the integer is always the same.

2. "%seq_file%->index = index;" looks like loff_t* to loff_t assignment. Is it?

Yes, this is a bug. I have corrected the specification in 'seq-index-fix' branch.

Actions #9

Updated by Ilja Zakharov about 7 years ago

  • Status changed from Resolved to Verified

Merged to master in 4fc472bf.

Actions #10

Updated by Ilja Zakharov about 7 years ago

  • Status changed from Verified to Closed
Actions

Also available in: Atom PDF