Project

General

Profile

Actions

Feature #11513

closed

Add pattern search to error traces comparison functions

Added by Anton Vasilyev 3 months ago. Updated about 2 months ago.

Status:
Closed
Priority:
High
Category:
Bridge
Target version:
Start date:
03/29/2022
Due date:
04/25/2022
% Done:

100%

Estimated time:
Published in build:

Description

It will be good for verification tool research to have ability to specify error marks by pattern search within witness or CPAchecker log, like currently implemented for Unknowns.

Basic usecase: to have ability to distinguish different Unsafes within implementation of new features for verification tool by specifying error message.


Related issues 1 (0 open1 closed)

Blocked by Klever - Feature #11514: Describe how to support new functions for unsafe marksRejected03/30/2022

Actions
Actions #1

Updated by Evgeny Novikov 3 months ago

  • Description updated (diff)
  • Category set to Bridge
  • Assignee set to Vladimir Gratinskiy
  • Priority changed from Normal to High

I would like to paraphrase the description. Quite often the same reasons are responsible for a lot of unsafes and there are some simple patterns (probably regular expressions) like for unknowns to classify corresponding unsafes. These patterns should be applied to all potentially visible contents of error traces including notes and warnings (Bridge does not deal with violation witnesses). Maybe this is quite a big deal for Bridge since it will be necessary to have another representation of error traces in addition to currently supported ones.

Actions #2

Updated by Evgeny Novikov 3 months ago

  • Blocked by Feature #11514: Describe how to support new functions for unsafe marks added
Actions #3

Updated by Evgeny Novikov 3 months ago

  • Assignee changed from Vladimir Gratinskiy to Evgeny Novikov
  • Target version set to 3.5

Let's me be a first user of a new subsection in the developer documentation that Vladimir will write for blocking issue #11514.

Actions #4

Updated by Evgeny Novikov 3 months ago

  • Assignee changed from Evgeny Novikov to Vladimir Gratinskiy

Currently related Bridge functionality is not designed in the way to support this easily. So Vladimir will have to enable this first. To ensure that this works, he can also complete the given task. Also, you can see my last note at #11514.

Actions #5

Updated by Vladimir Gratinskiy 2 months ago

  • Due date set to 04/25/2022
  • Status changed from New to Resolved
  • % Done changed from 0 to 100

Implemented in branch "bridge-11513".

Actions #6

Updated by Evgeny Novikov 2 months ago

It was fixed/improved in the same branch. CI has launched tests.

Actions #7

Updated by Evgeny Novikov 2 months ago

  • Status changed from Resolved to Closed

Tests passed, so I merged the branch to master in aebfa1cd0. Here is a mini how-to. You can create a new unsafe mark with regexp only in the full-weight mode (indeed, this has sense since they are not created by default and they will not be necessary too often). There you should select the regexp_match error traces comparison function. Then you need to specify an appropriate regexp. Take into account that flags re.S and re.M are used, so e.g. "__ab_c_size.*Field with size \d+ bit can't be written at offset \d+ bit of object -\d+ bit size" can match multiple lines where __ab_c_size will correspond to a call of that function and the last part of the regexp will correspond to the warning.

Note that it can take more time to associate unsafe marks using regexps, especially when you create them for the first time (Bridge generates appropriate caches then) and when you unset attribute "Program fragment" so that it is not used at association (this has sense, since regexps can spread across multiple drivers). Another small inconvenience is that you will likely see quite many dissimilar marks for unsafes if you will unset attribute "Program fragment" as suggested above. You can hide these marks by using an appropriate view.

Actions #8

Updated by Evgeny Novikov about 2 months ago

Vladimir fixed one minor bug - one could not edit unsafe marks with regular expressions in the lightweight mode. Now this works. The corresponding commit to master is 37427f973.

Actions

Also available in: Atom PDF