Skip to content

Latest commit

 

History

History
214 lines (169 loc) · 5.32 KB

FORMAT.md

File metadata and controls

214 lines (169 loc) · 5.32 KB

Configuration files format

Verification Priorities

The YAML format. An example:

priority:
   lists:
      - &1
         - <function>
         - <function>
         - ...

      - &2
         - <function>
         - <function>
         - <function>
         - ...

      ...

      - &n
         - <function>
         - <function>
         - ...

   colors:
        *1 : <color>
        *2 : <color>
        *3 : <color>
        ...
        *n : <color>

Where:

  • <function> - a function name, e.g., "main"
  • <color> - color for priority, e.g., "lightcyan"

The number of priorities is not fixed. The number of colors should correspond to the number of priorities. Color names can be taken from graphviz documentation. A function name can occur only once in configuration (should be unique).

The example for ext2 fs driver.

Issues

The YAML format. An example:

issues:
   <name>:
      description: <description>
      re: '<regexp>'
   <name>:
      description: <description>
      re: '<regexp>'
   ...

Where:

  • <name> - issue id number, e.g., '#41'
  • <description> - description, e.g., "Can't verify functions with allocation"
  • <regexp> - regular expression to check the body of a function, e.g., '\bmalloc\b'

Verification Status

The YAML format. An example:

done:
   - <function>
   - <function>
   ...

lemma-proof-required:
   - <function>
   - <function>
   ...

partial-specs:
   - <function>
   - <function>
   ...

specs-only:
   - <function>
   - <function>
   ...

Where:

  • done - list of fully-verified functions
  • lemma-proof-required - list of fully-verified functions, except proofs for lemmas they rely on
  • partial-specs - list of functions with draft contracts
  • specs-only - list of functions with contracts, that we can't prove for some reason
  • <function> - a function name, e.g., "main"

A function name can occur only once in configuration (should be unique).

The sample configuration for ext2 driver.

Extricate

The INI format. An example:

full=1
single=1
cache=0

plugin=inline
plugin-inline-text=begin^1^#define KERNRELEASE "TEST"

plugin=exec
plugin-exec-file=scripts/compile.sh

The configuration consists of the command line options of the tool. Arguments should be separated by new lines. Configuration flags (enable/disable arguments) should be equal either 1 (enabled) or 0 (disabled). A configuration file will be read automatically (of course, you can say directly which file to use through --config argument). Following command line arguments can redefine arguments from a configuration file.

An example.

Web

The INI format. An example:

kernel_dir   = /spec-utils/linux-4.17/
module_dir   = /spec-utils/linux-4.17/fs/ext2/
cache        = 1
cache_file   = /spec-utils/web/_web.graph.cache
out          = /spec-utils/web/
format       = svg

priority = 1
done     = 1

priority_config_file  = /spec-utils/config/priority_ext2.conf.sample
status_config_file    = /spec-utils/config/status_ext2.conf.sample
dbfile                = /spec-utils/web/ext2.db

The configuration consist from the following arguments:

  • kernel_dir - a path to the directory with kernel sources (absolute path)
  • module_dir - a path to the directory with module sources (absolute path)
  • cache - enable/disable caching
  • cache_file - a file for caching (absolute path). Option is required if cache enabled
  • out - a directory for storing tmp files (to store generated images)
  • format - default format for callgraph images. The same formats are available as in the graph tool, the format should be supported by the browser
  • priority - display priorities on the map
  • done - display verification status for functions on the map
  • priority_config_file - a path to the priority config file (absolute path). Option is required if priority enabled
  • status_config_file - a path to the status configuration file (absolute path). Option is required if status enabled
  • dbfile - a sqlite file for displaying addition information on right button (absolute path). Can be generated by the complexity_plan tool

An example.

Calls Status

The YAML format. An example:

functions:
   +/-:
      - copy_from_user
      - copy_to_user
      - put_cred
      - d_find_alias
      - get_cred
      - dput
      - dget
      - fget
      - fput
      - getxattr


   +:
      - memcpy
      - kfree
      - kmalloc
      - kzalloc
      - memset
      - memcpm
      - printk
      - SOCKET_I
      - atomic_inc
      - strcat
      - strcmp
      - strcpy
      - strncmp

macros:
   ready:
      - IS_RDONLY

   '!':
      - likely
      - unlikely
      - EXPORT_SYMBOL

At the top level, two keys are used - "functions" and "macros". At the third level, names of functions/macros should be used accordingly. Names should be unique. At the second level, arbitrary keys can be used. Keys from this level mark the corresponding macros and functions in the reports. Thus, in this example, the function memcpy in a report in the column Status will has value +, copy_from_user - +/-.