Inferred triggers for (\forall ... (\exists ...))

Apr 5, 2011 at 9:51 PM

I am working on writing a verified implementation of strspn, but I am experiencing some difficulty with verifying one of the post-condition assertions.

To simplify things a bit, consider:

#include <stddef.h>
#include <vcc.h>

_(pure) size_t strlen(const char *str _(ghost size_t nul_pos))
	_(requires \thread_local_array(str, nul_pos + 1))
	_(requires str[nul_pos] == '\0')
	_(reads \array_range(str, nul_pos + 1))
	_(ensures \result <= nul_pos)
	_(ensures str[\result] == '\0' && \forall size_t j; j < \result ==> str[j] != '\0')
	_(ensures \result == nul_pos <==> (\forall size_t j; j < nul_pos ==> str[j] != '\0'))
	_(ensures \forall size_t i; {\match_long(i)} i <= \result <==> (\forall size_t j; j < i ==> str[j] != '\0'))
	_(ensures \forall size_t i; {\match_long(i)} i == \result <==> (str[i] == '\0' && i <= \result))
{
	size_t i = 0;

	for (; str[i] != '\0'; ++i)
		_(invariant i <= nul_pos)
		_(invariant \forall size_t j; j < i ==> str[j] != '\0')
		(void)0;

	return i;
}

size_t strspn(const char *str, const char *skip_chars
		_(ghost size_t str_nul_pos) _(ghost size_t skip_chars_nul_pos))
	_(requires \thread_local_array(str, str_nul_pos + 1))
	_(requires \thread_local_array(skip_chars, skip_chars_nul_pos + 1))
	_(requires str[str_nul_pos] == '\0')
	_(requires skip_chars[skip_chars_nul_pos] == '\0')
	_(ensures \result <= strlen(str, str_nul_pos))
	_(ensures \forall size_t j; j < strlen(skip_chars, skip_chars_nul_pos) ==> str[\result] != skip_chars[j])
	_(ensures str[\result] == '\0' ==> \result == strlen(str, str_nul_pos))
	_(ensures \forall size_t l; l <= strlen(str, str_nul_pos) && (\forall size_t k; k < l ==> (\exists size_t j; j < strlen(skip_chars, skip_chars_nul_pos) && str[k] == skip_chars[j])) && (\forall size_t j; j < strlen(skip_chars, skip_chars_nul_pos) ==> str[l] != skip_chars[j]) ==> \result == l)
{
}

(The last ensures of strspn is line 33.)

I used VCC 2.1.40403.0 with the /dt:3 command line option and saw in the output:

test.c(33,107) : warning VC9122: inferred triggers at {:level 2}: {(&)skip_chars[j]} for '\exists size_t j; j < strlen(skip_chars, skip_chars_nul_pos) && str[k] == skip_chars[j])'
test.c(33,78) : warning VC9122: inferred triggers at {:level 2}: {<<$idx($ptr(^^i1, P#str), Q#k$2^33.78#tc1, ^^i1)>>} for '\forall size_t k; k < l ==> (\exists size_t j; j < strlen(skip_chars, skip_chars_nul_pos) && str[k] == skip_chars[j]))'

{(&)skip_chars[j]} looks right to me for '\exists size_t j; j < strlen(skip_chars, skip_chars_nul_pos) && str[k] == skip_chars[j])', but what does the trigger {<<$idx($ptr(^^i1, P#str), Q#k$2^33.78#tc1, ^^i1)>>} mean for '\forall size_t k; k < l ==> (\exists size_t j; j < strlen(skip_chars, skip_chars_nul_pos) && str[k] == skip_chars[j]))'?

Daniel

Coordinator
Apr 6, 2011 at 8:39 PM

Hi Daniel,

  "$idx(a, i, t)" is the internal representation of "&a[i]" for "t *a". The code which prints the inferred triggers only cares a bit to transform what it prints into C-like syntax (like "(&)a[j]"). The output here happens on a line with the comment "// this shouldn't happen
", so some further investigation might be necessary.

  I haven't closely looked into the exact postcondition you are trying to establish here, but things might simplify if you require "str_nul_pos" and "skip_chars_nul_pos" to be minimal identifying a null byte in the input string. (The second postcondition seems to need this property...).

Best, Mark

 

Apr 6, 2011 at 11:49 PM

I decided to try splitting the single ensures into two:

	_(ensures \forall size_t l; {\match_long(l)} l < strlen(str, str_nul_pos) && (\forall size_t k; {str[k]} k <= l ==> (\exists size_t j; j < strlen(skip_chars, skip_chars_nul_pos) && str[k] == skip_chars[j])) ==> l < \result)
	_(ensures \forall size_t l; l <= strlen(str, str_nul_pos) && (\forall size_t j; j < strlen(skip_chars, skip_chars_nul_pos) ==> str[l] != skip_chars[j]) ==> \result <= l)

The first one verifies, but I can't seem to get the second one to verify. If instead of the first \forall I use \exists, as in:

	_(ensures \exists size_t l; l <= strlen(str, str_nul_pos) && (\forall size_t j; j < strlen(skip_chars, skip_chars_nul_pos) ==> str[l] != skip_chars[j]) ==> \result <= l)

then VCC 2.1.40403.0 verifies that, too. The problem is that I can't use it to verify asserts of the form 'strspn(str, skip_chars, str_nul_pos, skip_chars_nul_pos) <= #'. I need to use \forall to verify these asserts:

	const char skip_chars[] = { ' ', '\t', '\r', '\n', '\0' };
	const char str1[] = { 'a', 'b', '\0' };
	const char str2[] = { ' ', 'a', '\0' };
	
	_(assert strspn(str1, skip_chars, 2, 4) <= 0)
	_(assert strspn(str2, skip_chars, 2, 4) <= 1)

By the way, I chose to require a position of a NUL char rather than the minimal position of a NUL char because I figured that it is an easier assumption to prove. All I need for the concept of "the string pointed to by a char pointer" to be well defined is that there exists a NUL char, and so far, VCC seems to be handling this well.

Daniel

Apr 7, 2011 at 12:53 AM

Here is my current implementation of strspn:

size_t strspn(const char *str, const char *skip_chars
		_(ghost size_t str_nul_pos) _(ghost size_t skip_chars_nul_pos))
{
	size_t i;

	for (i = 0; str[i] != '\0'; ++i)
		_(invariant i <= strlen(str, str_nul_pos))
		_(invariant \forall size_t l; l <= strlen(str, str_nul_pos) && (\forall size_t j; j < strlen(skip_chars, skip_chars_nul_pos) ==> str[l] != skip_chars[j]) ==> i <= l)
	{
		size_t j;
		int found = 0;
		
		for (j = 0; skip_chars[j] != '\0'; ++j)
			_(invariant j <= strlen(skip_chars, skip_chars_nul_pos))
			_(invariant !found)
			_(invariant \forall size_t k; k < j ==> str[i] != skip_chars[k])
			_(invariant str[i] != '\0')
		{
			if (str[i] == skip_chars[j])
			{
				found = !0;
				break;
			}
		}
		
		if (!found)
		{
			return i;
		}
	}

	return i;
}
Apr 9, 2011 at 1:48 AM

I'm still struggling with verifying that second post-condition;  I can't seem to get VCC to verify it.

To remove as much detail as possible and focus on just that post-condition, I have been playing with a toy function to return the least index of a non-digit character in a given array of n characters (or n if all characters are digits):

static const char digit_chars[10] = { '0', '1', '2', '3', '4', '5', '6', '7', '8', '9' };

size_t first_nondigit(const char *buf, size_t n)
	_(requires \thread_local_array(buf, n))
	_(ensures \result <= n)
	_(ensures \forall size_t l; l < n && (\forall size_t j; j < 10 ==> buf[l] != digit_chars[j]) ==> \result <= l);

 

How can I get VCC to verify the second post-condition?

Daniel