Support external function annotations

[misonijnik]

For a precise analysis of real-world program symbolic execution engine should be possible to execute external functions. Although there are executable code models for many commonly used external functions, some behaviors of external functions are difficult to model in this way. We want to add the ability to annotate external functions by specifying their behavior. For this purpose we propose to use the annotation format from the cooddy static analyzer project. At the initial stage we will support annotations like InitNull and Deref.

Annotations example with only InitNull and Deref annotations

{
  "malloc": [["InitNull"], []],
  "memccpy": [[], ["Deref"], ["Deref"], [],[]]
}

What do you think about this format of annotations?

[ladisgin]

Summary after online discussion

Need add to current annotation properties about function:

1. Is return determine value by parameter
2. Is change environment or global variables
3. Noreturn for function like 'abort' or 'exit'

It will be good make format more human-readable like next format:

{
    "z6myFoo5" : { // mangled name, can't get be user
        "name" : "myFoo5",
        "types" : ["int", "mystruct*", "int", "int"], // Maybe move it to annotation section. Problem with typedef, class etc
        "annotation" : [
            ["Result::$1 + $2 * $3"], // return
            [], // this
            [], // a
            []  // b
        ],
        "properties" : ["determ", "envs", "noreturn"]
    }
}

But it has several problem:

1. How people get mangled names
2. What do with user struct and typedefs

It can be solved by auto generate of template but it's hard get people to install and configure a tool for this.

[ladisgin]

Final format

1. mangled name as key
2. named fields for properties and annotation
3. annotation has same format as 'cooddy'
4. properties specified function behavior which does not depend on arguments and return
5. can be extend by new fields

{
    "z6myFoo5" : { // mangled name
        "annotation" : [
            ["Result::$1 + $2 * $3"], // return
            [], // this
            [], // a
            []  // b
        ],
        "properties" : ["determ", "envs", "noreturn"]
    }
}