goblint / analyzer Goto Github PK

... which is why the test script currently kills all goblints at the end (see here).

Use type-driven code generation to get rid of boilerplate (see ppx_deriving):

• yojson for output of domains values (see #210)
• show for output of domains values (see #213)
• eq, ord for domains (PR #227)
• hash: ppx_hash exists, but depends on and builds around Jane Street Base hash stuff, which conflicts with our base.ml..., and it doesn't seem to support all the primitive types eq and ord derivers do (e.g. char); alternatively implement own more direct deriver https://github.com/sim642/ppx_deriving_hash?
• relift (#1095)
• create ppx drivers for own ideas (e.g. names/lifting of modules)
  • Derive Product-, Record-domain (ppx-lattice branch, PR #1095)
  • Derive Flat- and Chain-Domain from variant types
  • Derive name () from Domain name
  • Derive Lifted functions

For example the following doesn't compile, but goblint doesn't say anything:

int f(int a, int b){
    int x = b; // this is bottom
    return a;
}
int main(){
    return f(1);
}

• Add option to use GCC to check whether the program compiles, and abort if if does not
• stop Goblint execution when Cil creates a Boo inline Assembly instruction.
  • In Cil: when this assembly instruction is produces, as of now, instead fail.

• update_suite.rb and pupdate_suite.rb have diverged - is there a reason for keeping the non-parallel version?
• failed tests should be printed as such right away, so that one can abort early
• exceptions should be detected
• there should be a timeout for each test
• tests that run with multiple configs (e.g. solver tests where each test runs with every solver)
• #41
• complaints of the verifier should also be taken into account (currently tests can succeed despite not having reached a fix-point)

For XML output printXML is used instead of toXML because toXML was too slow/memory intensive for large outputs.
The problem with removing it, is that it is used for result options indented, compact, html.

Refine the abstract values of function pointers by checking which functions in the C source code are compatible with regards to their type.

Note: Calling an unknown function pointer is currently unsound, as not all functions are abstractly "executed".

In general, we might a first flow-insensitive analysis for providing global-variants per type. These abstractions could then be used to refine top-values in a subsequent analysis.

and multithread.ml, of course!

Test 02-base/11-init_mainfun.c fails.

The following tests only fail for osx on travis but work locally and on linux:

$ ruby scripts/update_suite.rb
04/33 mutex/kernel_rc failed! ☠
04/34 mutex/kernel_nr failed! ☠
04/39 mutex/rw_lock_nr failed! ☠
04/40 mutex/rw_lock_rc failed! ☠
04/53 mutex/kernel-spinlock failed! ☠

These warnings are probably justified. I haven't tested this, but I believe flag == unflag (or some such thing with variables on both sides) will probably not be handled here. I wish there was some simple way to tell ocaml that Martin (almost certainly) intended the other semantics...

We have (circular) (32/64bit) intervals, but we don't handle all sizes and casts between them correctly.

We currently only output the line of an access.

For multiple accesses in one line it might be good to have:

• the starting index within the line

The current linux-headers.tbz file is missing compiler-gcc5.h, which makes the regression tests fail when running with cpp-5:

❯ ./goblint --enable kernel tests/regression/00-sanity/14-startstate.c
In file included from ./linux-headers/include/linux/compiler.h:54:0,
                 from ./linux-headers/include/linux/ioport.h:12,
                 from ./linux-headers/include/linux/device.h:16,
                 from tests/regression/00-sanity/14-startstate.c:2:
./linux-headers/include/linux/compiler-gcc.h:68:0: warning: "__weak" redefined
 #define __weak    __attribute__((weak))
 ^
<built-in>: note: this is the location of the previous definition
In file included from ./linux-headers/include/linux/compiler.h:54:0,
                 from ./linux-headers/include/linux/ioport.h:12,
                 from ./linux-headers/include/linux/device.h:16,
                 from tests/regression/00-sanity/14-startstate.c:2:
./linux-headers/include/linux/compiler-gcc.h:106:30: fatal error: linux/compiler-gcc5.h: No such file or directory
compilation terminated.
Goblint: Preprocessing failed.

There are 32 'experimental' options. Maybe those could be better classified or cleaned up.
The number of experimental options should be kept at a minimum.
Todo:

• Introduce additional categories:
  • witness
  • solver
  • context
  • incremental
  • output
• Sort experimental options into the categories
• Rename defaults.ml to options.ml
• Finalize options, so that they cannot be mutated after the solver started
• ana.warnings is used
• warnstyle only refers to race warnings

Related #192

Since 2e60f17, we have a few more uncalled functions. The pointer is put into a struct at ipmi_devintf.c:114, and then used later on. I'm not sure whether this function was previously called during the assignment or a few lines below where the struct containing that pointer is passed to the external function.

• Provide JSON-configurations for "commonly used configuration variables".
  • There should be a CI check to ensure they do not become outdated
• goblint --help Should mention example/meaningful configurations in the conf directory

Running the regression tests with intervals makes almost all the tests fail.

Examples:

• array index out of bounds
• segfaults: null-pointer access, ...?
• div by zero
• memory leaks
• undefined behavior (see ubsan)
• wrong API usage (use automatons)

Each warning should have tags/a category to be able to filter runtime errors/soundness warnings/assumptions etc.

CIL's CInt64 is only ok for constants that fit in OCaml's int64 (signed). Anything bigger silently overflows.
The constructor has a string option which should contain the original literal, but unfortunately it's always None.

The eclipse plugin is no longer supported.
It would be nice to have some plugin for:

• visual studio code
• sublime text
• vim/emacs
• ...

Happens when casting to unsigned long long, which happens a lot in kernel code. Added a simple test for this. Crash is in src/cdomains/intDomain.ml", line 534.

n/a

In tests/02_/01_, for example, the local variable 'i' will be added to the global invariant when processing the statement 'assert(i==7)' in multi-threaded mode. Why is that?

Some of the skipped tests throw exceptions because some configuration changed ("Unknown path ana.osek.tramp") or type errors ("Addr.type_offset: type error").

Privatization is a complicated and not well documented feature with strange effects.
In particular it seems to query globals before side-effects to them are generated? This causes non-termination for interval analysis on globals with the slr3 solver.

./goblint --enable ana.int.i⇡terval --sets solver slr3 tests/regression/04-mutex/01-simple_rc.c

Use something like ag "\(\*([^\*]|\*+[^\)]){500,}\*\)" to find bigger comments. Note that this doesn't work for cases in which a nested comment appears before the limit!

• Integers internal representation is int64 (signed)
• Interval32 -> Interval (I : S)
• Interval64 = Interval (Integers)
• add type argument to all int operations
• errors (e.g. Div_by_zero)? see #55
  • old: bottom
  • new: M.warn [Undefined] "div. by zero", top?
• get rid of Trier
• Big_int, uint?

• a simple example is test 6/20
• this is needed to make per-element locking and lockstep patterns useful in real code

Useful for:

• refactoring
• improvement in precision

Is marshalling the result hashtables good enough?

It is difficult to get the g2html tool to run. It would be nice to run it with just --enable g2html. The deafault location for the jar should be g2html/g2html.jar, but I'm not sure what other params I need to feed the analyzer.

Neither Chrome nor Safari can process the output by

goblint --set ana.activated "[['base', 'maylocks','thread-id-location']]" --sets result html knot_comb-3.c

on my sample file.

E.g. go to line 508, and try to see analysis results.

Who created this mess and why??

Test 02-base/10-init_allfuns.c needs to pass.

I disabled the test because it has been failing since commit 4cef73f. Remember to enable the test again once you fix the problem.

This will compile fine with gcc -std=c89 -pedantic (after removing the assert), and prints 0.

int main(void) {
  int a[42][42];
  int i, j;
  int *ptr;
  int x;

  for(i = 0; i < 42; i++) {
    for(j=0;j < 42; j++) {
      a[i][j] = 0;
    }
  }

  a[14][0] = 3;

  ptr = a[7];
  x = *(ptr+7);
  assert(x == 3); //FAIL
  printf("x is %d", x); // Will print 0
}

Our address domain has {&a[14][0]} for (ptr+7). This problem was hidden by the array domains so far, but after the changes in 1a4b6f0, we incorrectly output that the assert is true.

This is because for PlusPi we always add the integer to the first Index, thereby giving us
{&a[14][0]} for (ptr+7).

Cil's defaults are generated from src/machdep-ml.c.in and then stored in _build/machdep.ml.

• make Machdep.theMachine configurable in goblint
• provide default configurations {intel, arm} {32bit, 64bit} {linux, macOS}

Note: testing script probably needs some amending to recognize line numbers on a new line.

Edit: Since #338 we have a general system from warnings. What remains to be done is the chore of adding appropriate categories to some of the warnings.

E.g. ./goblint --enable ana.int.intervals ... just runs without any message (and without intervals), where it should abort and maybe suggest the option ana.int.interval.

These options exclude other options or have dependencies:

• warn if ana.int.interval is enabled but solver doesn't do widening:
  • EffectWCon and Worklist do not support widening.
  • Check other solvers whether they work with loops that modify ints
• warn if ana.osek.* is set but osek analysis isn't active
• Fail if one of the privatizations that require exact locksets (or must and may locksets) is active, but mutex is not path-sensitive

We have two machines here (one Linux, one MacOS), where due to the new requirement of having xml-light INSTALLED (as opposed to built next to Goblint), we can't build Goblint since ocamlfind can't find xml-light. Most likely a problem with xml-light, but a show-stopper for Goblint here.

For example

#include <stdio.h>
#include <string.h>
#include <pthread.h>

struct { int a; int b; } x;

void *f(void *arg){
  memcpy((void*)(&x.a), (void*)(&x.b), sizeof(int));
  return 0;
}

int main(){
  x.a = 1; x.b = 2;
  pthread_t id;
  pthread_create(&id, NULL, f, NULL);
  pthread_join (id, NULL);
  return 0;
}

./goblint --enable allglobs memcpy.c only gives

Memory location x.a (race with conf. 90)
  [email protected]:8 with {} (conf. 90)

When I set reachable to true for read accesses in mutex.ml, I get the expected

Memory location x.a (race with conf. 90)
  [email protected]:8 with {} (conf. 90)
  [email protected]:8 with {} (conf. 90)
Memory location x.b (safe)
  [email protected]:8 with {} (conf. 90)

However, this breaks tests/regression/05-lval_ls/17-per_elem_simp.c.

Introduced since commit 1450b8f.

$ goblint tests/regression/01-cpa/11-fun_ptrargs.c --debug
Failed to evaluate function expression assert (tests/regression/01-cpa/11-fun_ptrargs.c:28)
Failed to evaluate function expression assert (tests/regression/01-cpa/11-fun_ptrargs.c:32)
Failed to evaluate function expression assert (tests/regression/01-cpa/11-fun_ptrargs.c:33)
Failed to evaluate function expression set (tests/regression/01-cpa/11-fun_ptrargs.c:35)
Failed to evaluate function expression assert (tests/regression/01-cpa/11-fun_ptrargs.c:36)
Failed to evaluate function expression tes (tests/regression/01-cpa/11-fun_ptrargs.c:38)
Failed to evaluate function expression assert (tests/regression/01-cpa/11-fun_ptrargs.c:39)
Failed to evaluate function expression assert (tests/regression/01-cpa/11-fun_ptrargs.c:45)

Warnings are emitted at src/framework/multithread.ml:102.

Please ignore.

Whitespace:

• remove trailing whitespace
• remove trailing new lines
• fix mixed indentation
• fix indentation of comments for vim's foldmethod=indent to work

Unify code style. Use ocp-indent or maybe Mascot (problem: requires OCaml >= 4.0.0 & < 4.02.0).

The voglerr/goblint image was created manually - its latest commit is from June 2014...
We should use automated builds to keep this up to date.

The query system uses a variant type for the question and a polymorphic variant type for the result.

Problem Every query has only a subset of valid return variants. This information is not encoded in the type, i.e., every question might return any result.

Idea Use GADTs. Problem Subtyping (r can't be covariant): code, issue.

Idea Get rid of need for subtyping (the result type seems partially redundant anyway):

type 'd r = Result of 'd | Top | Bot
let rec query : type d. d t -> d r = ...