langston-barrett
commented
2 years ago After a bit more reflection I now think that the ideal input language for this feature would be more rich than what UC-Crux currently provides via the Postcond type. The ideal is probably closer to SAW's notion of a collection of overrides. For each external function, the user could provide n specifications, where a spec consists of:
- A precondition (the existing
Precondtype) - An optional postcondition (i.e., a summary of the function's effect on the program state)
- A soundness tag, one of
- Overapproximate
- Underapproximate
- Neither
- Both
The precondition would be a constraint on the program state which specifies when the spec applies (e.g., f returns a positive number, but only if given a positive number as an input). Together with these n specs, the user could provide the intended behavior if none of their preconditions match, which might be either (1) an error (like SAW does if no overrides match) or (2) fallback to the current unsound function-skipping behavior.
For example, the following is a spec for a division function, stating that the output is symbolic and non-negative if the numerator is non-negative and denominator is positive or if both the numerator is non-positive and denominator is negative.
- name: div
specs:
- # spec 1: non-negative / positive = non-negative
pre:
- args:
- # numerator
signed-greater-or-equal: 0
- # denominator
signed-greater: 0
post:
- ret:
symbolic:
signed-greater-or-equal: 0
- # spec 2: non-positive / negative = non-negative
pre:
- args:
- # numerator
signed-less-or-equal: 0
- # denominator
signed-less: 0
post:
- ret:
symbolic:
greater-or-equal: 0
# neither under-approximate nor over-approximate
soundness: neither
# failure to match all specs is an error (1), also see below
match-failure: errorIf the behavior in case of failure to match preconditions is an error, then UC-Crux could also use the specs to infer preconditions on callers of the external function, i.e., the caller should guarantee that it satisfies the intersection of the preconditions of the specs for the external function at the callsite. For example, in the above spec, match-failure: error indicates that it is an error to pass a denominator of zero (since doing so would not match the preconditions of any of the specs).
If the user doesn't provide a postcondition for an override, the default behavior would also be to fall back to the unsound skipping. It would only really make sense to provide such overrides if failure to match preconditions is treated as an error.
It would also be nice to provide a way to specify values that aren't concrete nor symbolic, but are derived from existing values. For instance, fgets(3) says:
char *fgets(char *restrict s, int size, FILE *restrict stream);
fgets() returns s on success, and NULL on error or when end of file occurs while no
characters have been read.which might be specified like so:
- name: fgets
specs:
- pre: {}
post:
- ret:
# NULL, i.e., EOF or error
constant: 0
- pre: {}
post:
- ret:
# s, i.e., success
arg: 0
soundness: neither
travitch
kquick
UC-Crux has the ability to skip over execution of declared but not defined functions, e.g., from a third-party library or libc. This is practical, but it has its disadvantages:
For libc functions in particular, we could manually implement overrides (in Haskell) for some of them. Sound overrides could live in
crucible-llvm, and unsound ones in UC-Crux. However, this takes considerable effort and still doesn't work for other third-party libraries.Instead, we should implement deserialization of function postconditions (#981), probably from YAML, along with specifications of whether the provided postconditions are overapproximate, underapproximate, both, or neither (for the sake of #932 and tracking of unsoundness). This would mostly require making non-GADT versions of UC-Crux's data structures and working out how to convert to/from them.