Open langston-barrett opened 1 year ago
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.)
We currently have three kinds of tests:
callgraph_test
that read Datalog relations into Python and make assertions about themrelation_property_test
that assert general features of the output of the analysisOnly 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
andFileCheck
could be useful.