Report Constraints

[mzuenni]

BAPCtools has a feature where validators are invoked with an additional argument --constraints_file <path> to allow the validator to report the bounds for all variables, and it would be nice if .ctd checkers would support this out of the box.

More precisely the validator can write a file to the given path containing the minimum and maximum values seen for all numbers read. Each line in the output is supposed to look like this:

<string identifier> <string name> <bool reached minimum> <bool reached maximum> <minimum allowed> <maximum allowed> <minimum seen> <maximum seen>

• <string identifier> is used to identify the corresponding token in the checker (for example by providing line:col but could also just be the name of the variable)
• <string name> is supposed to be the name of the variable
• <bool reached minimum> is 1 if the read value was equal to the lower bound at some point and else 0
• <bool reached maximum> is 1 if the read value was equal to the upper bound at some point and else 0
• <minimum allowed> is the minimum over all provided lower bounds for the variable
• <maximum allowed> is the maximum over all provided lower bounds for the variable
• <minimum seen> is the minimum that was read for the variable
• <maximum seen> is the maximum that was read for the variable

For example, the .ctd code INT(1, 1000, a) could generate this line:

a a 0 0 999 999 1 1000

The two zeros indicate that the minimum and maximum value were not reached (i.e. boolean false). The 999 999 indicate that a was read, and the smallest and largest value of a we encountered was 999. The final 1 1000 indicate the valid range of a.

Some more Notes:

• the bounds can be reported for FLOAT, FLOATP, and INT
• the bounds should only be reported if the variable has a name