Correct use of uberspark_uobjrtl_crt__strlen?

überSpark Framework üobject RTL
1

What is the proper way to use this function?

2

The crt uobjrtl function implementations and specifications are explicitly designed to work with the uberSpark verification process and will obey their functional correctness specifications as written.

As you can see from the speficiation of uberspark_uobjrtl_crt__strlen (in uobjrtl/crt/src/strlen.c) , the requires clause uses the Length_of_str_is predicate. This predicate is defined within uobjrtl/crt/include/string.h and establishes the validity of the input string memory locations, the final NULL termination character, and returns the length of the string.

This predicate allows us to verify the functional correctness of strlen implementation separately via deductive verification using weakest precondition calculus.

Further, the sources to strlen along with the function contract is passed through to the uobject memory value analysis phase where abstract interpretation is used to verify valid memory accesses of the entire uobject (including invoking strlen if present). This phase will trigger an error if the requires clause of strlen is not satisfied (e.g., by passing to a malformed string buffer to strlen, the validity of whose memory locations and resulting length cannot be established).

So, if the uobject memory access verification phase succeeeds, it means there are only valid uses of strlen. If there an invalid uses of strlen, the verification phase will report an error.

So, use strlen with a valid string buffer with valid length within a uobject so that the verification can succeed.

Examples of accesses which will pass verification follow:

int mylen;
mylen = uberspark_uobjrtl_crt__strlen("hello world");

Another example:

int mylen;
char buf[10]; 
uberspark_uobjrtl_crt__strcpy(buf, "hello"); 
mylen = uberspark_uobjrtl_crt__strlen(buf);

Hope this helps.

3

Thanks! In the two code examples, do I need to check mylen >=0 before using it? If I understand it correctly, I do not need to do it in uxmhf or uspark because they’ll be verified

4

You are correct. If you used either of the above two approaches, this should pass verification.

5

Well if the string is of length 0, then mylen will be 0, else it will be the length of the string.