Feature #2421: Add a verifier specific header for each error traces - Linux Driver Verification - Open-Source Projects

Actions

Copy link

Feature #2421

closed

Add a verifier specific header for each error traces

Added by Evgeny Novikov almost 13 years ago. Updated almost 13 years ago.

Status:

Closed

Priority:

Urgent

Assignee:

Evgeny Novikov

Category:

Statistics server

Start date:

02/10/2012

Due date:

% Done:

Estimated time:

Published in build:

e1279b7

Description

We have missed this earlier indeed. I found a hard-coded 'blast' verifier engine in KB routines that helped to process BLAST error traces and use such the circumstance:

return 1 if (call_stacks_ne($et, $kb_et));

while the correct one should be like this:

return 1 if (call_stacks_ne($et, 'engine1', $kb_et, 'engine2'));

('engine1' may equal to 'engine2').
This completely fails when an engine used isn't blast.
By means of a header specified for a error trace processed it'll be clear what engine should be used.

Related issues 1 (0 open — 1 closed)

Actions

Copy link

Updated by Evgeny Novikov almost 13 years ago

I suggest that a full fix requires rather much time (we should implement the 'engine' field, test it, update previously obtained results, test different combinations of engines, etc.). Because of our primary goal today is CPAchecker, I'm going to hard-code:

return 1 if (call_stacks_ne($et, 'cpachecker', $kb_et, 'cpacheker'));

Actions

Copy link

Updated by Evgeny Novikov almost 13 years ago

Priority changed from Urgent to High

I add this hack in commit 85a6d6b ("HACK! Hard code 'cpachecker' as a default KB error traces engine") of etv-redisign. So we're able to deal with cpachecker error traces at the moment. But it'll fail with the BLAST ones...

Actions

Copy link

Updated by Evgeny Novikov almost 13 years ago

Subject changed from Add a verifier field for KB records to Add a verifier specific hader for each error traces
Description updated (diff)

After all we decided:

Do not add a special field for verifier in KB records.
Instead we'll print a special header to each error trace. This header'll tell us what tool produces a given error trace (also a tool version may be useful, for instance, when a tool specific error trace format changes).
Create a cache of error traces in the common format. Both error trace visualizer and KB recalculator will use this cache instead of translation on fly. And a script that can convert all error traces from DB (from tables 'traces' and 'kb') to the common format on demand (I'm going to create a separate issue for this).

Actions

Copy link

Updated by Evgeny Novikov almost 13 years ago

Priority changed from High to Urgent

Without this issue there are a lot of problems with KB, ldv-upload and so on!

Actions

Copy link

Updated by Evgeny Novikov almost 13 years ago

Here are some SQL statements to fix up local databases (the order is important!):

Old CPAchecker error traces format where just a reference to CIL source file was specified. Just remove this reference, I advice you to remove such launches at all!
```
update traces set error_trace=substr(error_trace, locate('Line 0', error_trace)) where error_trace like 'Src%';
```

Add a header for CPAchecker error traces stored in results:

update traces set error_trace=concat('CPAchecker error trace v1.1\n', error_trace) where verifier like 'cpachecker';

The same for BLAST:

update traces set error_trace=concat('BLAST error trace v2.7\n', error_trace) where verifier like 'blast';

Add a header for CPAchecker error traces stored in KB:

update kb set error_trace=concat('CPAchecker error trace v1.1\n', error_trace) where error_trace like '-------%';

The same for BLAST:

update kb set error_trace=concat('BLAST error trace v2.7\n', error_trace) where error_trace not like 'CPAchecker %';

Scripts updating:

update kb set script="return 1 if (call_stacks_ne($et, $kb_et));" where script like "return 1 if (call_stacks_ne($et, 'cpachecker', $kb_et, 'cpachecker'));"

I'm going to apply them on QA for reference launches and for CPAchecker results on rothmans.
To update KB cache you should run:

LDVDB=ldv_db_3 LDVUSER=joker kb-recalc.pl --init-cache

Unfortunately without additional investigation and tuning scripts match different verifiers and different versions error traces not so good at the moment. This isn't very important for reference launches I guess and fixable for other cases.

Actions

Copy link