Project

General

Profile

Feature #9246

Get ready rule specifications for verification of C programs

Added by Evgeny Novikov 7 months ago. Updated 5 months ago.

Status:
Closed
Priority:
Urgent
Category:
Rule specifications
Target version:
Start date:
08/22/2018
Due date:
% Done:

0%

Estimated time:
Published in build:

Description

Regarding rule specifications and their base we just kept in mind an ability to verify C programs in addition to Linux kernel loadable modules. Since Klever 2.0 this ability should be supported that requires some changes. Among others they are:
  • Place rule specifications (they include all other specifications) into top-level directory specifications. Move file rule specs.json there and rename it to base.json.
  • Move files ldv-test.* from the top-level directory of the main verification job to appropriate place (likely to several jobs which need this).
  • Move generic:memory to linux:memory safety. The corresponding rule specification does too Linux specific and it can not be used for anything else.
  • Ditto move sync:race to linux:concurrency safety.
  • Move out all Linux specifics from verifier/*. Partially this was already done by Alexey Polushkin, but this breaks Linux stuff.
  • Get rid of two redundant parameters from job.json, namely rule specifications DB and verifier profiles DB.
  • Rename parameter rule specifications to requirements.
  • Support a requirements tree within former rule specifications.json to arrange them nicely, e.g.:
        "linux": {
          "decsription": "...", # Common description for all underlying requirements.
          "template": "...", # Common template for all underlying requirements.
          ...
          "concurrency safety": {...},
          ...
          "kernel": {
            ...
            "locking": {
              "mutex": {...},
              "rwlock": {...},
              "spinlock": {...}
            },
            ...
          },
          ...
          "memory safety": {...},
          ...
        }
    
  • Fix everything that rely upon changed things, e.g. environment model specifications, preset marks, tests and of course scripts.

If somebody has some notes, it is better to say them ASAP as starting from tomorrow everything mentioned will be implemented.

History

#1 Updated by Evgeny Novikov 7 months ago

Ilja Zakharov suggested to move all common directories and files like specifications and verifier profiles.json from specific preset job directories into the root preset directory. In addition, I suggest to organize preset jobs like requirements. So after all we will have something like:

jobs
  preset
    apache
    busybox
    linux
      3.14
      testing environment model specs
      testing rule specs
      validation
    requirements
    testing verifiers
    verifier profiles.json

#2 Updated by Ilja Zakharov 7 months ago

  • Status changed from New to Resolved

Implemented in Klever 2.0 branch. As the whole branch contains dramatic changes, this feature can also somewhere be not working.

#3 Updated by Evgeny Novikov 5 months ago

  • Status changed from Resolved to Closed

Branch klever-2.0 passed all tests and I merged it to master in 72be796e3 marked as v2.0rc1.

Also available in: Atom PDF