Bug #666: Strange error trace: incorrect model and blast lack - Linux Driver Verification - Open-Source Projects

Custom queries

Composite Backlog
LDV+BLAST
LDV-Git bugs

Actions

Copy link

Bug #666

closed

Strange error trace: incorrect model and blast lack

Added by Alexey Khoroshilov almost 14 years ago. Updated over 13 years ago.

Status:

Closed

Priority:

High

Assignee:

Pavel Shved

Category:

Infrastructure

Start date:

01/13/2011

Due date:

% Done:

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

Download all 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 open — 1 closed)

Related to Linux Driver Verification - Bug #680: BLAST should not ignore __blast_assert "function call" on stack overflow

Closed

Alexandr Strakh

01/17/2011

Actions

Issue # Delay: days Cancel

History
Notes
Property changes

Actions

Copy link

Updated by Evgeny Novikov almost 14 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

Copy link

Updated by Evgeny Novikov almost 14 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

Copy link

Updated by Pavel Shved almost 14 years ago

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

Could you please provide

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

Actions

Copy link

Updated by Alexey Khoroshilov almost 14 years ago

Pavel Shved wrote:

Could you please provide

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

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

How can I find these files?

Actions

Copy link

Updated by Pavel Shved almost 14 years ago

Alexey Khoroshilov wrote:

Pavel Shved wrote:

Could you please provide

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

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.

Actions

Copy link Download all files

Updated by Alexey Khoroshilov almost 14 years ago

File random.ko.linked.cbe.i random.ko.linked.cbe.i added
File random.ko.linked.ldv_main0_plain_sorted_withcheck.debug.gz random.ko.linked.ldv_main0_plain_sorted_withcheck.debug.gz added
Status changed from Feedback to Open

Pavel Shved wrote:

Could you please provide

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

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

Copy link

Updated by Evgeny Novikov almost 14 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

Copy link

Updated by Pavel Shved almost 14 years ago

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

Actions

Copy link

Updated by Pavel Shved almost 14 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:

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

I'd try to choose the second way.

Actions

Copy link

#10

Updated by Evgeny Novikov almost 14 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

Copy link

#11

Updated by Pavel Shved almost 14 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

Copy link

#12

Updated by Pavel Shved almost 14 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

Copy link

#13

Updated by Evgeny Novikov almost 14 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

Copy link

#14

Updated by Pavel Shved almost 14 years ago

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

Actions

Copy link

#15

Updated by Evgeny Novikov almost 14 years ago

Published in build set to 5ddd8

This commit in master 5ddd8 fixes the problem.

Actions

Copy link

#16

Updated by Alexey Khoroshilov over 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

Copy link

#17

Updated by Evgeny Novikov over 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

Copy link

#18

Updated by Evgeny Novikov over 13 years ago

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

Actions

Copy link

#19

Updated by Pavel Shved over 13 years ago

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

Actions

Copy link

#20

Updated by Pavel Shved over 13 years ago

Status changed from Open to Closed

Actions

Copy link

Also available in: Atom PDF

Project

General

Profile

Linux Driver Verification

Custom queries

Bug #666

Strange error trace: incorrect model and blast lack

Updated by Evgeny Novikov almost 14 years ago

Updated by Evgeny Novikov almost 14 years ago

Updated by Pavel Shved almost 14 years ago

Updated by Alexey Khoroshilov almost 14 years ago

Updated by Pavel Shved almost 14 years ago

Updated by Alexey Khoroshilov almost 14 years ago

Updated by Evgeny Novikov almost 14 years ago

Updated by Pavel Shved almost 14 years ago

Updated by Pavel Shved almost 14 years ago

Updated by Evgeny Novikov almost 14 years ago

Updated by Pavel Shved almost 14 years ago

Updated by Pavel Shved almost 14 years ago

Updated by Evgeny Novikov almost 14 years ago

Updated by Pavel Shved almost 14 years ago

Updated by Evgeny Novikov almost 14 years ago

Updated by Alexey Khoroshilov over 13 years ago

Updated by Evgeny Novikov over 13 years ago

Updated by Evgeny Novikov over 13 years ago

Updated by Pavel Shved over 13 years ago

Updated by Pavel Shved over 13 years ago