diff --git a/tests/regression/my_regexec_pointer_diff_cast.c b/tests/regression/my_regexec_pointer_diff_cast.c new file mode 100644 index 0000000..766ff54 --- /dev/null +++ b/tests/regression/my_regexec_pointer_diff_cast.c @@ -0,0 +1,53 @@ +/* + * Small reproducer for the CodeHawk-C my_regexec failure seen in SPEC + * CPU2017 perlbench. + * + * The important shape is: + * + * unsigned_len_arg(..., end - begin) + * + * where begin and end are both char pointers. In C, end - begin is pointer + * subtraction with signed ptrdiff_t result. Passing it to an unsigned length + * parameter creates the same kind of signed-to-unsigned-cast proof obligation + * as perlbench's: + * + * MgBYTEPOS(mg, sv, strbeg, strend - strbeg) + * + * CH-C generated a valid obligation for that cast, but then crashed while + * reconstructing an API expression for the upper-bound invariant because it + * treated the pointer difference as ordinary arithmetic XMinus and attempted + * integer promotion on (char *) and (char *). + * + * Ref: https://github.com/static-analysis-engineering/CodeHawk-C/issues/75 + */ + +#include + +typedef unsigned long STRLEN; + +static STRLEN consume_len(const char *base, STRLEN len) { + return base[len] == '\0' ? len : len + 1; +} + +STRLEN my_regexec_repro(const char *strbeg, const char *strend) { + return consume_len(strbeg, strend - strbeg); +} + +STRLEN my_regexec_repro_with_guard(const char *strbeg, const char *strend) { + if (strend < strbeg) { + return 0; + } + + return consume_len(strbeg, strend - strbeg); +} + +STRLEN my_regexec_source_workaround(const char *strbeg, const char *strend) { + if (strend < strbeg) { + return 0; + } + + { + STRLEN len = (STRLEN)(strend - strbeg); + return consume_len(strbeg, len); + } +} diff --git a/tests/regression/tests.json b/tests/regression/tests.json index eb816ce..be51529 100644 --- a/tests/regression/tests.json +++ b/tests/regression/tests.json @@ -19,6 +19,14 @@ "safe": 37 } }, + { + "filename": "my_regexec_pointer_diff_cast.c", + "expected": { + "safe": 106, + "open": 9 + }, + "goal": "improve" + }, { "filename": "test_POCheckInitialized.c", "expected": {