Project

General

Profile

Actions

Bug #666

closed

Strange error trace: incorrect model and blast lack

Added by Alexey Khoroshilov over 13 years ago. Updated about 13 years ago.

Status:
Closed
Priority:
High
Assignee:
Category:
Infrastructure
Start date:
01/13/2011
Due date:
% Done:

0%

Estimated time:
Detected in build:
2afcef4
Platform:
Published in build:
5ddd8

Description

Lines 493 and below are shown as part of ldv_spin_lock_irqsave() that is incorrect. It should be at the same level as line 492, where ldv_spin_lock_irqsave() is called.

492 - blast_must_tmp__36 = ldv_spin_lock_irqsave();
      {
3127   blast_must_tmp__1433 = ldv_lock;
3127   assert(blast_must_tmp__1433 != 1);
3127   + __blast_assert();
493    - blast_must_tmp__37 = llvm_cbe_r_addr;
         blast_must_tmp__38 =* (blast_must_tmp__37 ).field8;

Files

error_trace.tar.gz (16.4 KB) error_trace.tar.gz Alexey Khoroshilov, 01/13/2011 11:00 AM
random.ko.linked.cbe.i (642 KB) random.ko.linked.cbe.i Alexey Khoroshilov, 01/15/2011 12:13 AM
random.ko.linked.ldv_main0_plain_sorted_withcheck.debug.gz (151 KB) random.ko.linked.ldv_main0_plain_sorted_withcheck.debug.gz Alexey Khoroshilov, 01/15/2011 12:13 AM

Related issues 1 (0 open1 closed)

Related to Linux Driver Verification - Bug #680: BLAST should not ignore __blast_assert "function call" on stack overflowClosedAlexandr Strakh01/17/2011

Actions
Actions #1

Updated by Evgeny Novikov over 13 years ago

  • Category set to Infrastructure
  • Status changed from New to Open
  • Assignee set to Evgeny Novikov
  • Priority changed from Normal to High

I'll try to fix it quickly. Seems that it's simple bug.

Actions #2

Updated by Evgeny Novikov over 13 years ago

  • Subject changed from Incorrect visualization of error trace to Strange error trace: incorrect model and blast lack
After reviewing of error trace it becomes clear that in fact error trace visualizer does just that what it's asked to do.
I see 2 problems:
  • By some reasons blast skips the first blast_assert (you may see it in attached trace).
  • It seems that 43_1 model is incorrect because of ldv_spin_unlock_irqrestore doesn't do needed actions. Instead it calls to undefined (why it so?..) function ldv_spin_unlock_irqrestore_1.
    More detailed complex analysis is needed.
Actions #3

Updated by Pavel Shved over 13 years ago

  • Status changed from Open to Feedback
  • Assignee changed from Evgeny Novikov to Pavel Shved

Could you please provide

  1. the file that was passed to BLAST, and the command line options
  2. the full report that was generated by blast (*.debug.gz)

?

Actions #4

Updated by Alexey Khoroshilov over 13 years ago

Pavel Shved wrote:

Could you please provide

  1. the file that was passed to BLAST, and the command line options
  2. the full report that was generated by blast (*.debug.gz)

How can I find these files?

Actions #5

Updated by Pavel Shved over 13 years ago

Alexey Khoroshilov wrote:

Pavel Shved wrote:

Could you please provide

  1. the file that was passed to BLAST, and the command line options
  2. the full report that was generated by blast (*.debug.gz)

How can I find these files?

You can retrieve command-line options from log (if debug level is at least 20), search for pblast.opt.*driver.ko, pick a line with the proper main function.
You'll see a line the report will be written to nearby, that's the debug.gz file.

Updated by Alexey Khoroshilov over 13 years ago

Pavel Shved wrote:

Could you please provide

  1. the file that was passed to BLAST, and the command line options

pblast.opt /home/tester/.ldv/ldv/envs/1/work/work-4162cf64973df51fc885825bc9ca4d055891c49f/drivers/char/random.c/work/current--X--commands.xml--X--defaultshadows--X--43_1/artificial_env_1/csd_deg_dscv/2/dscv_tempdir/dscv/cmdfiles/rcv/43_1/preprocessed/random.ko.linked.cbe.i -predH 7 -craig 2 -ignoredupfn -nosserr -skipnorm -main ldv_main0_plain_sorted_withcheck -L llvm_cbe_LDV_ERROR -cldepth 0 -lattice -include-lattice symb -stop-sep -merge bdd -enable-recursion -fdepth 5

  1. the full report that was generated by blast (*.debug.gz)

By the way, there are some warnings in the log:

Use of uninitialized value $line in concatenation (.) or string at ldv/opt/shared/perl/LDV/Utils.pm line 174.
Use of uninitialized value $line in scalar chomp at ldv/opt/shared/perl/LDV/Utils.pm line 175.

Actions #7

Updated by Evgeny Novikov over 13 years ago

Alexey Khoroshilov wrote:

By the way, there are some warnings in the log:
[...]

I have already asked Alexander, he said that it is concerned with watcher. This doesn't lead to the given problem.

Actions #8

Updated by Pavel Shved over 13 years ago

Warnings are fixed in 1a50730. Going to check what's there about the bigger problem.

Actions #9

Updated by Pavel Shved over 13 years ago

LDV-Git runs BLAST with a limited function call stack. According to the report, when BLAST first encountered __blast_assert function call (that's a function call, as seen in the trace), it decided not to descend into it due to "stack overflow".

There are two ways to fix it:

  1. Fix Error-trace virualizer to take only the last __blast_assert() into account
  2. Fix BLAST to descend into __blast_assert always.

I'd try to choose the second way.

Actions #10

Updated by Evgeny Novikov over 13 years ago

I suggest that BLAST should print some comments for such functions like for function with undefined bodies:

FunctionCall(blast_must_tmp__132@pppox_init =
sock_register(&(pppox_proto_family)))
LDV: undefined function called: sock_register

May be so:
LDV: reach the function call stack limit: <the limit>

Otherwise every time when the given limit will be reached (it's just a "luck" that for this example it's meaningful __blast_assert function) error trace visualization will fail.

Actions #11

Updated by Pavel Shved over 13 years ago

Okay. So we have two problems here. The first one is that I overlooked the comments to be left, if a function body is not traversed into in a trace. This is to be fixed sooner.

The second one is that BLAST doesn't error-check error locations when stack capabilities, imposed by the -fdepth option, are full. This problem is tracked in bug #680.

Actions #12

Updated by Pavel Shved about 13 years ago

I can't reproduce the bug.
I have 64-bit architecture, and BLAST fails with Predicate index less than zero, this is a known 64-bit-related bug related to aspectator yielding large numbers instead of negative ints.

Please, Alexey, could you check if the issue still appears? Before you run, please, remove drv-env-gen folder and check it out again! (Aspectator failed on my machine if I didn't do that).

Actions #13

Updated by Evgeny Novikov about 13 years ago

This should be closed because of Alexander did it. I think that 43 model problems will be addressed later when we'll deal with it.

Actions #14

Updated by Pavel Shved about 13 years ago

Why should it be closed? What commit has fixed it? O_o

Actions #15

Updated by Evgeny Novikov about 13 years ago

  • Published in build set to 5ddd8

This commit in master 5ddd8 fixes the problem.

Actions #16

Updated by Alexey Khoroshilov about 13 years ago

The fix works well. The only cosmetic change I would propose is to fix a description shown to an end user.
/* The function call is skipped due to stack overflow. / is a misleading.
I believe a more appropriate text could be:
/
The function call is skipped to reduce time of verification according to '-fdepth XXX' option. */

Actions #17

Updated by Evgeny Novikov about 13 years ago

To do this again both fix of blast and fix of error-trace-visualizer should be done.
Nowadays blast doesn't print XXX:

FunctionCall(level7())
LDV: skipping call to function due to stack overflow: level7

Error-trace-visualizer doesn't take into account anything that follows after the second ':' at all.

Actions #18

Updated by Evgeny Novikov about 13 years ago

We may do it unless we forget the topic...

Actions #19

Updated by Pavel Shved about 13 years ago

Ok, since the fix works well, closing. We'll discuss the stack overflow message in bug #926.

Actions #20

Updated by Pavel Shved about 13 years ago

  • Status changed from Open to Closed
Actions

Also available in: Atom PDF