Correctness tests

[langston-barrett]

We currently have three kinds of tests:

1. Python correctness tests like callgraph_test that read Datalog relations into Python and make assertions about them
2. Property tests like relation_property_test that assert general features of the output of the analysis
3. Assertions in the Datalog code which are checked during property tests

Only the first type checks (and documents) the intended behavior of specific groups of rules in the analysis, and we have really limited numbers of those tests. For rules that contribute somewhat indirectly or infrequently to the analysis output, it's hard to say what they're intended to do or if they're doing it correctly (e.g., the rules dealing with pass-by-value semantics).

We should expand the number of these kinds of tests. However, it's kind of a pain to write them in Python (it's very "imperative", rather than "decarative"). I'm not sure what the best solution is, but I think perhaps lit and FileCheck could be useful.

[langston-barrett]

A particularly nice way to do this might be through specially-treated C functions embedded into test programs, like so:

#include <stdio.h>
#include <stdlib.h>

#include "assert.h"

int main() {
  char c = 0;
  assert_points_to_something(&c);
}

where assert.h is:

#ifdef RUN
void assert_points_to_something(void *p, ...) {}
void assert_reachable(void) {}
#else
extern void assert_points_to_something(void *p, ...);
extern void assert_reachable(void);
#endif

Then the Datalog analysis could incorporate a few special assertion relations that implement the semantics of these special functions. (We might want to prefix them by __cclyzer or something to avoid possible name collisions.)